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