equal
deleted
inserted
replaced
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" "name" "trm" |
19 | Lam "ty" "name" "trm" |
20 print_theorems |
|
21 |
20 |
22 primrec |
21 primrec |
23 rfv_kind :: "kind \<Rightarrow> atom set" |
22 rfv_kind :: "kind \<Rightarrow> atom set" |
24 and rfv_ty :: "ty \<Rightarrow> atom set" |
23 and rfv_ty :: "ty \<Rightarrow> atom set" |
25 and rfv_trm :: "trm \<Rightarrow> atom set" |
24 and rfv_trm :: "trm \<Rightarrow> atom set" |
31 | "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})" |
30 | "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})" |
32 | "rfv_trm (Const i) = {atom i}" |
31 | "rfv_trm (Const i) = {atom i}" |
33 | "rfv_trm (Var x) = {atom x}" |
32 | "rfv_trm (Var x) = {atom x}" |
34 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)" |
33 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)" |
35 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})" |
34 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})" |
36 print_theorems |
|
37 |
35 |
38 instantiation kind and ty and trm :: pt |
36 instantiation kind and ty and trm :: pt |
39 begin |
37 begin |
40 |
38 |
41 primrec |
39 primrec |