forked from ucsd-progsys/liquidhaskell
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPrelude.hquals
45 lines (33 loc) · 1.41 KB
/
Prelude.hquals
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
//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 True1(v:GHC.Types.Bool) : (v)
qualif False1(v:GHC.Types.Bool) : (~ 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 runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])