equal
deleted
inserted
replaced
6 atom_decl ident |
6 atom_decl ident |
7 |
7 |
8 nominal_datatype lf: |
8 nominal_datatype lf: |
9 kind = |
9 kind = |
10 Type |
10 Type |
11 | KPi "ty" n::"name" k::"kind" bind n in k |
11 | KPi "ty" n::"name" k::"kind" binds n in k |
12 and ty = |
12 and ty = |
13 TConst "ident" |
13 TConst "ident" |
14 | TApp "ty" "trm" |
14 | TApp "ty" "trm" |
15 | TPi "ty" n::"name" ty::"ty" bind n in ty |
15 | TPi "ty" n::"name" ty::"ty" binds n in ty |
16 and trm = |
16 and trm = |
17 Const "ident" |
17 Const "ident" |
18 | Var "name" |
18 | Var "name" |
19 | App "trm" "trm" |
19 | App "trm" "trm" |
20 | Lam' "ty" n::"name" t::"trm" bind n in t |
20 | Lam' "ty" n::"name" t::"trm" binds n in t |
21 |
21 |
22 abbreviation |
22 abbreviation |
23 KPi_syn::"name \<Rightarrow> ty \<Rightarrow> kind \<Rightarrow> kind" ("\<Pi>[_:_]._" [100,100,100] 100) |
23 KPi_syn::"name \<Rightarrow> ty \<Rightarrow> kind \<Rightarrow> kind" ("\<Pi>[_:_]._" [100,100,100] 100) |
24 where |
24 where |
25 "\<Pi>[x:A].K \<equiv> KPi A x K" |
25 "\<Pi>[x:A].K \<equiv> KPi A x K" |