src/HOL/Codegenerator_Test/Generate.thy
author haftmann
Fri Nov 26 12:03:18 2010 +0100 (2010-11-26)
changeset 40711 81bc73585eec
parent 37825 adc1143bc1a8
child 50629 264ece81df93
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 *}
     5 
     6 theory Generate
     7 imports Candidates
     8 begin
     9 
    10 subsection {* Check whether generated code compiles *}
    11 
    12 text {*
    13   If any of the checks fails, inspect the code generated
    14   by a corresponding @{text export_code} command.
    15 *}
    16 
    17 export_code _ checking SML OCaml? Haskell? Scala?
    18 
    19 end