author | wneuper <Walther.Neuper@jku.at> |
Fri, 05 Aug 2022 08:45:37 +0200 | |
changeset 60516 | 795d1352493a |
parent 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@60516 | 9 |
"----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------"; |
walther@60317 | 10 |
"-----------------------------------------------------------------------------------------------"; |
walther@60317 | 11 |
"-----------------------------------------------------------------------------------------------"; |
walther@60317 | 12 |
"-----------------------------------------------------------------------------------------------"; |
walther@60317 | 13 |
|
Walther@60516 | 14 |
"----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------"; |
Walther@60516 | 15 |
"----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------"; |
Walther@60516 | 16 |
"----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------"; |
walther@60317 | 17 |
|
Walther@60509 | 18 |
fun test thy t = |
Walther@60516 | 19 |
writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, Calc_Binop.simplify @{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>; |