13 (SML) "char" |
13 (SML) "char" |
14 and (OCaml) "char" |
14 and (OCaml) "char" |
15 and (Haskell) "Prelude.Char" |
15 and (Haskell) "Prelude.Char" |
16 and (Scala) "Char" |
16 and (Scala) "Char" |
17 |
17 |
18 setup {* |
18 setup \<open> |
19 fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] |
19 fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] |
20 #> String_Code.add_literal_list_string "Haskell" |
20 #> String_Code.add_literal_list_string "Haskell" |
21 *} |
21 \<close> |
22 |
22 |
23 code_printing |
23 code_printing |
24 class_instance char :: equal \<rightharpoonup> |
24 class_instance char :: equal \<rightharpoonup> |
25 (Haskell) - |
25 (Haskell) - |
26 | constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup> |
26 | constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup> |
105 and (Scala) infixl 4 "<" |
105 and (Scala) infixl 4 "<" |
106 and (Eval) infixl 6 "<" |
106 and (Eval) infixl 6 "<" |
107 | constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup> |
107 | constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup> |
108 (SML) "!((_ : string) <= _)" |
108 (SML) "!((_ : string) <= _)" |
109 and (OCaml) "!((_ : string) <= _)" |
109 and (OCaml) "!((_ : string) <= _)" |
110 -- {* Order operations for @{typ String.literal} work in Haskell only |
110 -- \<open>Order operations for @{typ String.literal} work in Haskell only |
111 if no type class instance needs to be generated, because String = [Char] in Haskell |
111 if no type class instance needs to be generated, because String = [Char] in Haskell |
112 and @{typ "char list"} need not have the same order as @{typ String.literal}. *} |
112 and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close> |
113 and (Haskell) infix 4 "<=" |
113 and (Haskell) infix 4 "<=" |
114 and (Scala) infixl 4 "<=" |
114 and (Scala) infixl 4 "<=" |
115 and (Eval) infixl 6 "<=" |
115 and (Eval) infixl 6 "<=" |
116 | constant "Orderings.less :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup> |
116 | constant "Orderings.less :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup> |
117 (SML) "!((_ : string) < _)" |
117 (SML) "!((_ : string) < _)" |