equal
deleted
inserted
replaced
1 theory LF |
1 theory LF |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 declare [[STEPS = 9]] |
5 declare [[STEPS = 20]] |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 atom_decl ident |
8 atom_decl ident |
9 |
9 |
10 nominal_datatype kind = |
10 nominal_datatype kind = |
11 Type |
11 Type |
12 | KPi "ty" n::"name" k::"kind" bind n in k |
12 | KPi "ty" n::"name" k::"kind" bind n in k |
13 and ty = |
13 and ty = |
14 TConst "ident" |
14 TConst "ident" |
15 | TApp "ty" "trm" |
15 | TApp "ty" "trm" |
16 | TPi "ty" n::"name" t::"ty" bind n in t |
16 | TPi "ty" n::"name" ty::"ty" bind n in ty |
17 and trm = |
17 and trm = |
18 Const "ident" |
18 Const "ident" |
19 | Var "name" |
19 | Var "name" |
20 | App "trm" "trm" |
20 | App "trm" "trm" |
21 | Lam "ty" n::"name" t::"trm" bind n in t |
21 | Lam "ty" n::"name" t::"trm" bind n in t |
22 |
22 |
23 thm kind_ty_trm.supp |
23 (*thm kind_ty_trm.supp*) |
24 |
|
25 |
|
26 |
|
27 |
24 |
28 |
25 |
29 end |
26 end |
30 |
27 |
31 |
28 |