changeset 2093 | 751d1349329b |
parent 2092 | c0ab7451b20d |
parent 2091 | 1f38489f1cf0 |
child 2094 | 56b849d348ae |
child 2095 | ae94bae5bb93 |
2092:c0ab7451b20d | 2093:751d1349329b |
---|---|
1 theory ExLF |
|
2 imports "../NewParser" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 atom_decl ident |
|
7 |
|
8 nominal_datatype kind = |
|
9 Type |
|
10 | KPi "ty" n::"name" k::"kind" bind_set n in k |
|
11 and ty = |
|
12 TConst "ident" |
|
13 | TApp "ty" "trm" |
|
14 | TPi "ty" n::"name" t::"ty" bind_set n in t |
|
15 and trm = |
|
16 Const "ident" |
|
17 | Var "name" |
|
18 | App "trm" "trm" |
|
19 | Lam "ty" n::"name" t::"trm" bind_set n in t |
|
20 |
|
21 thm kind_ty_trm.supp |
|
22 |
|
23 end |
|
24 |
|
25 |
|
26 |
|
27 |