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