671 and (Scala) infixl 7 "+" |
671 and (Scala) infixl 7 "+" |
672 | constant String.literal_of_asciis \<rightharpoonup> |
672 | constant String.literal_of_asciis \<rightharpoonup> |
673 (SML) "!(String.implode/ o List.map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))" |
673 (SML) "!(String.implode/ o List.map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))" |
674 and (OCaml) "!(let xs = _ |
674 and (OCaml) "!(let xs = _ |
675 and chr k = |
675 and chr k = |
676 let l = Big'_int.int'_of'_big'_int k |
676 let l = Z.to'_int k |
677 in if 0 <= l && l < 128 |
677 in if 0 <= l && l < 128 |
678 then Char.chr l |
678 then Char.chr l |
679 else failwith \"Non-ASCII character in literal\" |
679 else failwith \"Non-ASCII character in literal\" |
680 in String.init (List.length xs) (List.nth (List.map chr xs)))" |
680 in String.init (List.length xs) (List.nth (List.map chr xs)))" |
681 and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)" |
681 and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)" |
682 and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))" |
682 and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))" |
683 | constant String.asciis_of_literal \<rightharpoonup> |
683 | constant String.asciis_of_literal \<rightharpoonup> |
684 (SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)" |
684 (SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)" |
685 and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in |
685 and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in |
686 if k < 128 then Big'_int.big'_int'_of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])" |
686 if k < 128 then Z.of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])" |
687 and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))" |
687 and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))" |
688 and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))" |
688 and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))" |
689 | class_instance String.literal :: equal \<rightharpoonup> |
689 | class_instance String.literal :: equal \<rightharpoonup> |
690 (Haskell) - |
690 (Haskell) - |
691 | constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup> |
691 | constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup> |