equal
deleted
inserted
replaced
108 using rev2_rev'[OF assms] rev_length[OF assms] assms |
108 using rev2_rev'[OF assms] rev_length[OF assms] assms |
109 by (cases "Array.length h a = 0", auto simp add: Array.length_def |
109 by (cases "Array.length h a = 0", auto simp add: Array.length_def |
110 subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims) |
110 subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims) |
111 (drule sym[of "List.length (Array.get h a)"], simp) |
111 (drule sym[of "List.length (Array.get h a)"], simp) |
112 |
112 |
113 definition "example = (Array.of_list [1::nat, 2, 3, 4, 5, 6, 7, 8, 9, 10] \<guillemotright>= (\<lambda>a. rev a 0 9))" |
113 definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))" |
114 |
114 |
115 export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp? |
115 export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp? |
116 |
116 |
117 end |
117 end |