src/HOL/Codegenerator_Test/Code_Test_Scala.thy
author desharna
Mon, 22 Sep 2014 15:01:27 +0200
changeset 58417 fa50722ad6cb
parent 58348 2d47c7d10b62
child 58520 a4d1f8041af0
permissions -rw-r--r--
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
     1
(*  Title:      Code_Test_Scala.thy
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 Scala
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
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
     7
theory Code_Test_Scala imports Code_Test begin 
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 Scala
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 [Scala] "14 + 7 * -12 :: integer"
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
    12
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
    13
end