equal
deleted
inserted
replaced
16 \<Omega> | KFun kind kind |
16 \<Omega> | KFun kind kind |
17 |
17 |
18 nominal_datatype ty = |
18 nominal_datatype ty = |
19 TVar tvar |
19 TVar tvar |
20 | TFun ty ty |
20 | TFun ty ty |
21 | TAll a::tvar kind t::ty bind a in t |
21 | TAll a::tvar kind t::ty bind a in t |
22 | TEx a::tvar kind t::ty bind a in t |
22 | TEx a::tvar kind t::ty bind a in t |
23 | TLam a::tvar kind t::ty bind a in t |
23 | TLam a::tvar kind t::ty bind a in t |
24 | TApp ty ty |
24 | TApp ty ty |
25 | TRec trec |
25 | TRec trec |
26 and trec = |
26 and trec = |
27 TRNil |
27 TRNil |
28 | TRCons label ty trec |
28 | TRCons label ty trec |
29 |
29 |
30 nominal_datatype trm = |
30 nominal_datatype trm = |
31 Var var |
31 Var var |
32 | Lam x::var ty t::trm bind x in t |
32 | Lam x::var ty t::trm bind x in t |
33 | App trm trm |
33 | App trm trm |
34 | Dot trm label |
34 | Dot trm label |
35 | LAM a::tvar kind t::trm bind a in t |
35 | LAM a::tvar kind t::trm bind a in t |
36 | APP trm ty |
36 | APP trm ty |
37 | Pack ty trm |
37 | Pack ty trm |
38 | Unpack a::tvar x::var trm t::trm bind a x in t |
38 | Unpack a::tvar x::var trm t::trm bind a x in t |
39 | Rec rec |
39 | Rec rec |
40 and rec = |
40 and rec = |
41 RNil |
41 RNil |
42 | RCons label trm rec |
42 | RCons label trm rec |
43 |
43 |
44 |
44 |
|
45 thm ty_trec.distinct |
|
46 thm ty_trec.induct |
|
47 thm ty_trec.inducts |
|
48 thm ty_trec.exhaust |
|
49 thm ty_trec.strong_exhaust |
|
50 thm ty_trec.fv_defs |
|
51 thm ty_trec.bn_defs |
|
52 thm ty_trec.perm_simps |
|
53 thm ty_trec.eq_iff |
|
54 thm ty_trec.fv_bn_eqvt |
|
55 thm ty_trec.size_eqvt |
|
56 thm ty_trec.supports |
|
57 thm ty_trec.fsupp |
|
58 thm ty_trec.supp |
|
59 thm ty_trec.fresh |
45 |
60 |
|
61 thm trm_rec.distinct |
|
62 thm trm_rec.induct |
|
63 thm trm_rec.inducts |
|
64 thm trm_rec.exhaust |
|
65 thm trm_rec.strong_exhaust |
|
66 thm trm_rec.fv_defs |
|
67 thm trm_rec.bn_defs |
|
68 thm trm_rec.perm_simps |
|
69 thm trm_rec.eq_iff |
|
70 thm trm_rec.fv_bn_eqvt |
|
71 thm trm_rec.size_eqvt |
|
72 thm trm_rec.supports |
|
73 thm trm_rec.fsupp |
|
74 thm trm_rec.supp |
|
75 thm trm_rec.fresh |
46 |
76 |
47 end |
77 end |
48 |
78 |
49 |
79 |
50 |
80 |