changeset 58039 | 469a375212c1 |
child 58348 | 2d47c7d10b62 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Mon Aug 25 09:40:50 2014 +0200 @@ -0,0 +1,15 @@ +(* Title: Code_Test_GHC.thy + Author: Andreas Lochbihler, ETH Zurich + +Test case for test_code on GHC +*) + +theory Code_Test_GHC imports Code_Test begin + +definition id_integer :: "integer \<Rightarrow> integer" where "id_integer = id" + +test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC + +eval_term "14 + 7 * -12 :: integer" in GHC + +end