src/HOL/Codegenerator_Test/Generate_Pretty.thy
author haftmann
Fri Nov 26 12:03:18 2010 +0100 (2010-11-26)
changeset 40711 81bc73585eec
parent 37825 adc1143bc1a8
child 42842 6ef538f6a8ab
permissions -rw-r--r--
globbing constant expressions use more idiomatic underscore rather than star
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 header {* Pervasive test of code generator using pretty literals *}
     5 
     6 theory Generate_Pretty
     7 imports Candidates_Pretty
     8 begin
     9 
    10 lemma [code, code del]: "nat_of_char = nat_of_char" ..
    11 lemma [code, code del]: "char_of_nat = char_of_nat" ..
    12 lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
    13 lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" ..
    14 
    15 subsection {* Check whether generated code compiles *}
    16 
    17 text {*
    18   If any of the checks fails, inspect the code generated
    19   by a corresponding @{text export_code} command.
    20 *}
    21 
    22 export_code _ checking SML OCaml? Haskell? Scala?
    23 
    24 end