equal
deleted
inserted
replaced
38 char |
38 char |
39 |
39 |
40 code_reserved Scala |
40 code_reserved Scala |
41 char |
41 char |
42 |
42 |
43 definition implode :: "string \<Rightarrow> String.literal" where |
|
44 "implode = STR" |
|
45 |
|
46 code_reserved SML String |
43 code_reserved SML String |
47 |
44 |
48 code_printing |
45 code_printing |
49 constant implode \<rightharpoonup> |
46 constant String.implode \<rightharpoonup> |
50 (SML) "String.implode" |
47 (SML) "String.implode" |
51 and (OCaml) "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)" |
48 and (OCaml) "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)" |
52 and (Haskell) "_" |
49 and (Haskell) "_" |
53 and (Scala) "!(\"\" ++/ _)" |
50 and (Scala) "!(\"\" ++/ _)" |
54 | constant explode \<rightharpoonup> |
51 | constant String.explode \<rightharpoonup> |
55 (SML) "String.explode" |
52 (SML) "String.explode" |
56 and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])" |
53 and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])" |
57 and (Haskell) "_" |
54 and (Haskell) "_" |
58 and (Scala) "!(_.toList)" |
55 and (Scala) "!(_.toList)" |
59 |
56 |