equal
deleted
inserted
replaced
57 lemma [code]: |
57 lemma [code]: |
58 "size (as :: 'a iarray) = 0" |
58 "size (as :: 'a iarray) = 0" |
59 by (cases as) simp |
59 by (cases as) simp |
60 |
60 |
61 lemma [code]: |
61 lemma [code]: |
62 "iarray_size f as = Suc (size_list f (IArray.list_of as))" |
62 "size_iarray f as = Suc (size_list f (IArray.list_of as))" |
63 by (cases as) simp |
63 by (cases as) simp |
64 |
64 |
65 lemma [code]: |
65 lemma [code]: |
66 "rec_iarray f as = f (IArray.list_of as)" |
66 "rec_iarray f as = f (IArray.list_of as)" |
67 by (cases as) simp |
67 by (cases as) simp |