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
wenzelm@59720
     1
(*  Title:      HOL/Codegenerator_Test/Code_Test_Scala.thy
Andreas@58039
     2
    Author:     Andreas Lochbihler, ETH Zurich
Andreas@58039
     3
Andreas@58039
     4
Test case for test_code on Scala
Andreas@58039
     5
*)
Andreas@58039
     6
Andreas@61856
     7
theory Code_Test_Scala imports  "../Library/Code_Test" "../GCD" begin 
Andreas@58039
     8
haftmann@58520
     9
declare [[scala_case_insensitive]]
haftmann@58520
    10
Andreas@58039
    11
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
Andreas@58039
    12
Andreas@58348
    13
value [Scala] "14 + 7 * -12 :: integer"
Andreas@58039
    14
Andreas@61856
    15
test_code -- \<open>Tests for the serialisation of @{const gcd} on @{typ integer}\<close>
Andreas@61856
    16
  "gcd 15 10 = (5 :: integer)"
Andreas@61856
    17
  "gcd 15 (- 10) = (5 :: integer)"
Andreas@61856
    18
  "gcd (- 10) 15 = (5 :: integer)"
Andreas@61856
    19
  "gcd (- 10) (- 15) = (5 :: integer)"
Andreas@61856
    20
  "gcd 0 (- 10) = (10 :: integer)"
Andreas@61856
    21
  "gcd (- 10) 0 = (10 :: integer)"
Andreas@61856
    22
  "gcd 0 0 = (0 :: integer)"
Andreas@61856
    23
in Scala
Andreas@61856
    24
Andreas@58039
    25
end