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