equal
deleted
inserted
replaced
16 |
16 |
17 text \<open>Monadic heap actions either produce values |
17 text \<open>Monadic heap actions either produce values |
18 and transform the heap, or fail\<close> |
18 and transform the heap, or fail\<close> |
19 datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option" |
19 datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option" |
20 |
20 |
21 lemma [code, code del]: |
21 declare [[code drop: "Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term"]] |
22 "(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" |
|
23 .. |
|
24 |
22 |
25 primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where |
23 primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where |
26 [code del]: "execute (Heap f) = f" |
24 [code del]: "execute (Heap f) = f" |
27 |
25 |
28 lemma Heap_cases [case_names succeed fail]: |
26 lemma Heap_cases [case_names succeed fail]: |