1 (* Title: HOL/Library/Code_Char.thy
3 Author: Florian Haftmann
6 header {* Code generation of pretty characters (and strings) *}
9 imports Plain "~~/src/HOL/List"
12 declare char.recs [code func del] char.cases [code func del]
15 "size (c\<Colon>char) = 0"
19 "char_size (c\<Colon>char) = 0"
28 fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"]
29 #> add_literal_list_string "Haskell"
32 code_instance char :: eq
41 code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
42 (SML "!((_ : char) = _)")
43 (OCaml "!((_ : char) = _)")
44 (Haskell infixl 4 "==")