isabelle: src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy@8e4d542f041b (annotated)

59720 f893472fff31 proper headers; wenzelm parents: 58626 diff changeset	1	(* Title: HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	2	Author: Andreas Lochbihler, ETH Zurich
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	3
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	4	Test case for test_code on SMLNJ
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	5	*)
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	6
68155 8b50f29a1992 new tool Code_Lazy Andreas Lochbihler parents: 66453 diff changeset	7	theory Code_Test_SMLNJ imports "HOL-Library.Code_Test" Code_Lazy_Test begin
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	8
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	9	test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	10
58348 2d47c7d10b62 add target language evaluators for the value command; Andreas Lochbihler parents: 58039 diff changeset	11	value [SMLNJ] "14 + 7 * -12 :: integer"
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	12
68155 8b50f29a1992 new tool Code_Lazy Andreas Lochbihler parents: 66453 diff changeset	13	test_code "stake 10 (cycle ''ab'') = ''ababababab''" in SMLNJ
8b50f29a1992 new tool Code_Lazy Andreas Lochbihler parents: 66453 diff changeset	14
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	15	end

author	paulson <lp15@cam.ac.uk>
	Wed, 25 Mar 2020 12:37:57 +0000
changeset 71591	8e4d542f041b
parent 68155	8b50f29a1992
permissions	-rw-r--r--