equal
deleted
inserted
replaced
104 *} |
104 *} |
105 |
105 |
106 code_const arbitrary |
106 code_const arbitrary |
107 (Haskell target_atom "(error \"arbitrary\")") |
107 (Haskell target_atom "(error \"arbitrary\")") |
108 |
108 |
|
109 code_reserved SML Fail |
|
110 code_reserved Haskell error |
109 |
111 |
110 subsection {* Operational equality for code generation *} |
112 subsection {* Operational equality for code generation *} |
111 |
113 |
112 subsubsection {* eq class *} |
114 subsubsection {* eq class *} |
113 |
115 |
167 (Haskell -) |
169 (Haskell -) |
168 |
170 |
169 code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" |
171 code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" |
170 (Haskell infixl 4 "==") |
172 (Haskell infixl 4 "==") |
171 |
173 |
|
174 code_reserved Haskell |
|
175 Eq eq |
172 |
176 |
173 subsection {* normalization by evaluation *} |
177 subsection {* normalization by evaluation *} |
174 |
178 |
175 lemma eq_refl: "eq x x" |
179 lemma eq_refl: "eq x x" |
176 unfolding eq_def .. |
180 unfolding eq_def .. |