equal
deleted
inserted
replaced
23 unfolding char_of_int_def by (simp add: fun_eq_iff) |
23 unfolding char_of_int_def by (simp add: fun_eq_iff) |
24 |
24 |
25 code_const int_of_char and char_of_int |
25 code_const int_of_char and char_of_int |
26 (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") |
26 (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") |
27 (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)") |
27 (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)") |
28 (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . fromInteger)") |
28 (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)") |
29 (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))") |
29 (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))") |
30 |
30 |
31 end |
31 end |