equal
deleted
inserted
replaced
2 Author: Andreas Lochbihler, ETH Zurich |
2 Author: Andreas Lochbihler, ETH Zurich |
3 |
3 |
4 Test case for test_code on GHC |
4 Test case for test_code on GHC |
5 *) |
5 *) |
6 |
6 |
7 theory Code_Test_GHC imports "../Library/Code_Test" begin |
7 theory Code_Test_GHC imports "../Library/Code_Test" "../GCD" begin |
8 |
8 |
9 test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC |
9 test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC |
10 |
10 |
11 value [GHC] "14 + 7 * -12 :: integer" |
11 value [GHC] "14 + 7 * -12 :: integer" |
12 |
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 GHC |
|
22 |
13 end |
23 end |