author | blanchet |
Tue, 07 Jun 2011 11:13:52 +0200 | |
changeset 43236 | a1a0dcbeb785 |
parent 42842 | 6ef538f6a8ab |
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