equal
deleted
inserted
replaced
7 |
7 |
8 signature HOLOGIC = |
8 signature HOLOGIC = |
9 sig |
9 sig |
10 val termC: class |
10 val termC: class |
11 val termS: sort |
11 val termS: sort |
12 val termTVar: typ |
12 val termT: typ |
13 val boolT: typ |
13 val boolT: typ |
14 val false_const: term |
14 val false_const: term |
15 val true_const: term |
15 val true_const: term |
16 val mk_setT: typ -> typ |
16 val mk_setT: typ -> typ |
17 val dest_setT: typ -> typ |
17 val dest_setT: typ -> typ |
73 |
73 |
74 (* basics *) |
74 (* basics *) |
75 |
75 |
76 val termC: class = "term"; |
76 val termC: class = "term"; |
77 val termS: sort = [termC]; |
77 val termS: sort = [termC]; |
78 |
78 val termT = TypeInfer.anyT termS; |
79 val termTVar = TVar (("'a", 0), termS); |
|
80 |
79 |
81 |
80 |
82 (* bool and set *) |
81 (* bool and set *) |
83 |
82 |
84 val boolT = Type ("bool", []); |
83 val boolT = Type ("bool", []); |