src/HOL/Codegenerator_Test/Code_Test_Scala.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 61856 4b1b85f38944
child 63167 0909deb8059b
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/Codegenerator_Test/Code_Test_Scala.thy
     2     Author:     Andreas Lochbihler, ETH Zurich
     3 
     4 Test case for test_code on Scala
     5 *)
     6 
     7 theory Code_Test_Scala imports  "../Library/Code_Test" "../GCD" begin 
     8 
     9 declare [[scala_case_insensitive]]
    10 
    11 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
    12 
    13 value [Scala] "14 + 7 * -12 :: integer"
    14 
    15 test_code -- \<open>Tests for the serialisation of @{const gcd} on @{typ integer}\<close>
    16   "gcd 15 10 = (5 :: integer)"
    17   "gcd 15 (- 10) = (5 :: integer)"
    18   "gcd (- 10) 15 = (5 :: integer)"
    19   "gcd (- 10) (- 15) = (5 :: integer)"
    20   "gcd 0 (- 10) = (10 :: integer)"
    21   "gcd (- 10) 0 = (10 :: integer)"
    22   "gcd 0 0 = (0 :: integer)"
    23 in Scala
    24 
    25 end