| author | wenzelm |
| Thu, 16 Sep 2021 17:23:54 +0200 | |
| changeset 60405 | d4ebe139100d |
| parent 60401 | 54d17d6d4245 |
| child 60509 | 2e0b7ca391dc |
| permissions | -rw-r--r-- |
| walther@60317 | 1 |
(* Title: "ProgLang/calculate.sml" |
| walther@60317 | 2 |
Author: Walther Neuper 2021 |
| walther@60317 | 3 |
(c) copyright due to lincense terms. |
| walther@60317 | 4 |
*) |
| walther@60317 | 5 |
|
| walther@60317 | 6 |
"-----------------------------------------------------------------------------------------------"; |
| walther@60317 | 7 |
"table of contents -----------------------------------------------------------------------------"; |
| walther@60317 | 8 |
"-----------------------------------------------------------------------------------------------"; |
| walther@60317 | 9 |
"----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; |
| walther@60317 | 10 |
"-----------------------------------------------------------------------------------------------"; |
| walther@60317 | 11 |
"-----------------------------------------------------------------------------------------------"; |
| walther@60317 | 12 |
"-----------------------------------------------------------------------------------------------"; |
| walther@60317 | 13 |
|
| walther@60317 | 14 |
"----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; |
| walther@60317 | 15 |
"----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; |
| walther@60317 | 16 |
"----------- RE-BUILD fun eval_binop -----------------------------------------------------------"; |
| walther@60317 | 17 |
|
| walther@60401 | 18 |
fun test thy t = writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul thy t))); |
| walther@60317 | 19 |
|
| walther@60401 | 20 |
test \<^theory> \<^term>\<open>10 + 20 :: real\<close>; |
| walther@60401 | 21 |
test \<^theory> \<^term>\<open>10 - 20 :: real\<close>; |
| walther@60401 | 22 |
test \<^theory> \<^term>\<open>10 * 20 :: real\<close>; |
| wenzelm@60405 | 23 |
test \<^theory> \<^term>\<open>10 \<up> 20 :: real\<close>; |
| walther@60401 | 24 |
|
| walther@60401 | 25 |
test \<^theory> \<^term>\<open>10 + 20 :: int\<close>; |
| walther@60401 | 26 |
test \<^theory> \<^term>\<open>10 - 20 :: int\<close>; |
| walther@60401 | 27 |
test \<^theory> \<^term>\<open>10 * 20 :: int\<close>; |
| walther@60401 | 28 |
|
| walther@60401 | 29 |
test \<^theory> \<^term>\<open>10 + 20 :: nat\<close>; |
| walther@60401 | 30 |
test \<^theory> \<^term>\<open>10 - 20 :: nat\<close>; |
| walther@60401 | 31 |
test \<^theory> \<^term>\<open>10 * 20 :: nat\<close>; |