equal
deleted
inserted
replaced
11 atom_decl var |
11 atom_decl var |
12 atom_decl tvar |
12 atom_decl tvar |
13 atom_decl label |
13 atom_decl label |
14 |
14 |
15 nominal_datatype kind = |
15 nominal_datatype kind = |
16 \<Omega> | KFun kind kind |
16 \<Omega> |
|
17 | KFun kind kind |
17 |
18 |
18 nominal_datatype ty = |
19 nominal_datatype ty = |
19 TVar tvar |
20 TVar tvar |
20 | TFun ty ty |
21 | TFun ty ty |
21 | TAll a::tvar kind t::ty bind a in t |
22 | TAll a::tvar kind t::ty bind a in t |
38 | Unpack a::tvar x::var trm t::trm bind a x in t |
39 | Unpack a::tvar x::var trm t::trm bind a x in t |
39 | Rec rec |
40 | Rec rec |
40 and rec = |
41 and rec = |
41 RNil |
42 RNil |
42 | RCons label trm rec |
43 | RCons label trm rec |
43 |
|
44 |
44 |
45 thm ty_trec.distinct |
45 thm ty_trec.distinct |
46 thm ty_trec.induct |
46 thm ty_trec.induct |
47 thm ty_trec.inducts |
47 thm ty_trec.inducts |
48 thm ty_trec.exhaust |
48 thm ty_trec.exhaust |