changeset 58348 | 2d47c7d10b62 |
parent 58039 | 469a375212c1 |
child 58414 | f945e7af0d27 |
58347:272ad6a47d6d | 58348:2d47c7d10b62 |
---|---|
8 |
8 |
9 definition id_integer :: "integer \<Rightarrow> integer" where "id_integer = id" |
9 definition id_integer :: "integer \<Rightarrow> integer" where "id_integer = id" |
10 |
10 |
11 test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC |
11 test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC |
12 |
12 |
13 eval_term "14 + 7 * -12 :: integer" in GHC |
13 value [GHC] "14 + 7 * -12 :: integer" |
14 |
14 |
15 end |
15 end |