equal
deleted
inserted
replaced
162 definition upd' where |
162 definition upd' where |
163 [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()" |
163 [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()" |
164 hide (open) const upd' |
164 hide (open) const upd' |
165 lemma [code func]: |
165 lemma [code func]: |
166 "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a" |
166 "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a" |
167 apply (simp add: upd'_def monad_simp) |
167 by (simp add: upd'_def monad_simp upd_return) |
168 oops |
|
169 |
168 |
170 |
169 |
171 subsubsection {* SML *} |
170 subsubsection {* SML *} |
172 |
171 |
173 code_type array (SML "_/ array") |
172 code_type array (SML "_/ array") |