src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 58889 5b7a9633cfa8
child 63167 0909deb8059b
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
haftmann@31378
     1
haftmann@31378
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@24195
     3
wenzelm@58889
     4
section {* Pervasive test of code generator *}
haftmann@24195
     5
haftmann@51161
     6
theory Generate_Binary_Nat
haftmann@51161
     7
imports
haftmann@51161
     8
  Candidates
haftmann@51161
     9
  "~~/src/HOL/Library/AList_Mapping"
haftmann@51161
    10
  "~~/src/HOL/Library/Finite_Lattice"
haftmann@51161
    11
  "~~/src/HOL/Library/Code_Binary_Nat"
haftmann@24195
    12
begin
haftmann@24195
    13
haftmann@37745
    14
text {*
haftmann@37824
    15
  If any of the checks fails, inspect the code generated
haftmann@37824
    16
  by a corresponding @{text export_code} command.
haftmann@37745
    17
*}
haftmann@37745
    18
haftmann@58678
    19
export_code _ checking SML OCaml? Haskell? Scala
haftmann@25616
    20
haftmann@24195
    21
end