equal
deleted
inserted
replaced
1 header {* CPS transformation of Danvy and Filinski *} |
1 header {* CPS transformation of Danvy and Filinski *} |
2 theory CPS3_DanvyFilinski imports Lt begin |
2 theory CPS3_DanvyFilinski imports Lt begin |
3 |
3 |
4 nominal_primrec |
4 nominal_function |
5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
5 CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100) |
6 and |
6 and |
7 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
7 CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100) |
8 where |
8 where |
9 "eqvt k \<Longrightarrow> (x~)*k = k (x~)" |
9 "eqvt k \<Longrightarrow> (x~)*k = k (x~)" |