blob: b4e1cb2c2f42ca2c4ee0d5e37df9e3ef64655057 (
plain)
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
|
abstract Math = {
flags startcat = Prop ;
cat
Prop ; Exp ;
fun
And, Or, If : Prop -> Prop -> Prop ;
Zero : Exp ;
Successor : Exp -> Exp ;
Sum, Product : Exp -> Exp -> Exp ;
Even, Odd, Prime : Exp -> Prop ;
Equal, Less, Greater, Divisible : Exp -> Exp -> Prop ;
cat
Var ;
fun
X, Y : Var ;
EVar : Var -> Exp ;
EInt : Int -> Exp ;
ANumberVar : Var -> Exp ;
TheNumberVar : Var -> Exp ;
}
|