| author | wneuper <Walther.Neuper@jku.at> |
| Thu, 04 Aug 2022 12:48:37 +0200 | |
| changeset 60509 | 2e0b7ca391dc |
| parent 60405 | d4ebe139100d |
| child 60516 | 795d1352493a |
| 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@60509 | 18 |
fun test thy t = |
| Walther@60509 | 19 |
writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul @{context} t)));
|
| walther@60317 | 20 |
|
| walther@60401 | 21 |
test \<^theory> \<^term>\<open>10 + 20 :: real\<close>; |
| walther@60401 | 22 |
test \<^theory> \<^term>\<open>10 - 20 :: real\<close>; |
| walther@60401 | 23 |
test \<^theory> \<^term>\<open>10 * 20 :: real\<close>; |
| wenzelm@60405 | 24 |
test \<^theory> \<^term>\<open>10 \<up> 20 :: real\<close>; |
| walther@60401 | 25 |
|
| 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 |
test \<^theory> \<^term>\<open>10 * 20 :: int\<close>; |
| walther@60401 | 29 |
|
| walther@60401 | 30 |
test \<^theory> \<^term>\<open>10 + 20 :: nat\<close>; |
| walther@60401 | 31 |
test \<^theory> \<^term>\<open>10 - 20 :: nat\<close>; |
| walther@60401 | 32 |
test \<^theory> \<^term>\<open>10 * 20 :: nat\<close>; |