equal
deleted
inserted
replaced
110 subarray_def rev.simps[where j=0] elim!: effect_elims) |
110 subarray_def rev.simps[where j=0] elim!: effect_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.make 10 id \<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 |
118 |
118 |