equal
deleted
inserted
replaced
1 section "Immutable Arrays with Code Generation" |
1 section \<open>Immutable Arrays with Code Generation\<close> |
2 |
2 |
3 theory IArray |
3 theory IArray |
4 imports Main |
4 imports Main |
5 begin |
5 begin |
6 |
6 |
41 by (cases as) (simp add: map_nth) |
41 by (cases as) (simp add: map_nth) |
42 |
42 |
43 end |
43 end |
44 |
44 |
45 |
45 |
46 subsection "Code Generation" |
46 subsection \<open>Code Generation\<close> |
47 |
47 |
48 code_reserved SML Vector |
48 code_reserved SML Vector |
49 |
49 |
50 code_printing |
50 code_printing |
51 type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector" |
51 type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector" |