packages feed

liquidhaskell-0.6.0.0: include/Prelude.hquals

//BOT: Do not delete EVER!

qualif Bot(v:@(0))    : (0 = 1) 
qualif Bot(v:obj)     : (0 = 1) 
qualif Bot(v:a)       : (0 = 1) 
qualif Bot(v:bool)    : (0 = 1) 
qualif Bot(v:int)     : (0 = 1) 

qualif CmpZ(v:a)      : (v <  0) 
qualif CmpZ(v:a)      : (v <= 0)
qualif CmpZ(v:a)      : (v >  0)
qualif CmpZ(v:a)      : (v >= 0)
qualif CmpZ(v:a)      : (v  = 0)
qualif CmpZ(v:a)      : (v != 0)

qualif Cmp(v:a, x:a)  : (v <  x) 
qualif Cmp(v:a, x:a)  : (v <= x)
qualif Cmp(v:a, x:a)  : (v >  x)
qualif Cmp(v:a, x:a)  : (v >= x)
qualif Cmp(v:a, x:a)  : (v  = x)
qualif Cmp(v:a, x:a)  : (v != x)

// qualif CmpZ(v:a)        : v [ < ; <= ; > ; >= ; = ; != ] 0
// qualif Cmp(v:a,x:a)     : v [ < ; <= ; > ; >= ; = ; != ] x
// qualif Cmp(v:int,x:int) : v [ < ; <= ; > ; >= ; = ; != ] x


qualif One(v:int)     : v = 1
qualif True(v:bool)   : (? v) 
qualif False(v:bool)  : ~ (? v) 
qualif True1(v:GHC.Types.Bool)   : (Prop(v))
qualif False1(v:GHC.Types.Bool)  : (~ Prop(v))


constant papp1 : func(1, [Pred @(0); @(0); bool])
qualif Papp(v:a,p:Pred a) : (papp1(p, v))

constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])
qualif Papp2(v:a,x:b,p:Pred a b) : (papp2(p, v, x))

qualif Papp3(v:a,x:b, y:c, p:Pred a b c) : (papp3(p, v, x, y))
constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])

// qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)
constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])


constant Prop : func(0, [GHC.Types.Bool; bool])
constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])