(* Author: Florian Haftmann, TU Muenchen *)
section ‹Pervasive test of code generator›
theory Generate
imports
"Candidates"
"HOL-Library.AList_Mapping"
"HOL-Library.Finite_Lattice"
"Go.Go_Setup"
begin
text ‹
If any of the checks fails, inspect the code generated
by a corresponding ‹export_code› command.
›
export_code _ checking Go (infinite_type "stream")
end
¤ Dauer der Verarbeitung: 0.3 Sekunden
¤
*© Formatika GbR, Deutschland
