author | bulwahn |
Wed, 18 May 2011 15:45:33 +0200 | |
changeset 42842 | 6ef538f6a8ab |
parent 40711 | 81bc73585eec |
child 43317 | f9283eb3a4bf |
permissions | -rw-r--r-- |
(* Author: Florian Haftmann, TU Muenchen *) header {* Pervasive test of code generator using pretty literals *} theory Generate_Pretty imports Candidates_Pretty begin lemma [code, code del]: "nat_of_char = nat_of_char" .. lemma [code, code del]: "char_of_nat = char_of_nat" .. subsection {* Check whether generated code compiles *} text {* If any of the checks fails, inspect the code generated by a corresponding @{text export_code} command. *} export_code _ checking SML OCaml? Haskell? Scala? end