src/HOL/Library/Code_Char_ord.thy
author bulwahn
Wed May 18 15:45:33 2011 +0200 (2011-05-18)
changeset 42841 9079f49053e5
child 42857 1e1b74448f6b
permissions -rw-r--r--
adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
bulwahn@42841
     1
(*  Title:      HOL/Library/Code_Char_ord.thy
bulwahn@42841
     2
    Author:     Lukas Bulwahn, Florian Haftmann, Rene Thiemann
bulwahn@42841
     3
*)
bulwahn@42841
     4
bulwahn@42841
     5
header {* Code generation of orderings for pretty characters *}
bulwahn@42841
     6
bulwahn@42841
     7
theory Code_Char_ord
bulwahn@42841
     8
imports Code_Char Char_ord
bulwahn@42841
     9
begin
bulwahn@42841
    10
  
bulwahn@42841
    11
code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
bulwahn@42841
    12
  (SML "!((_ : char) <= _)")
bulwahn@42841
    13
  (OCaml "<=")
bulwahn@42841
    14
  (Haskell infix 4 "<=")
bulwahn@42841
    15
  (Scala infixl 4 "<=")
bulwahn@42841
    16
  (Eval infixl 6 "<=")
bulwahn@42841
    17
bulwahn@42841
    18
code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
bulwahn@42841
    19
  (SML "!((_ : char) < _)")
bulwahn@42841
    20
  (OCaml "<")
bulwahn@42841
    21
  (Haskell infix 4 "<")
bulwahn@42841
    22
  (Scala infixl 4 "<")
bulwahn@42841
    23
  (Eval infixl 6 "<")
bulwahn@42841
    24
bulwahn@42841
    25
end