1 (* Title: "ProgLang/calculate.sml"
2 Author: Walther Neuper 2021
3 (c) copyright due to lincense terms.
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
10 "-----------------------------------------------------------------------------------------------";
11 "-----------------------------------------------------------------------------------------------";
12 "-----------------------------------------------------------------------------------------------";
14 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
15 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
16 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
19 writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul @{context} t)));
21 test \<^theory> \<^term>\<open>10 + 20 :: real\<close>;
22 test \<^theory> \<^term>\<open>10 - 20 :: real\<close>;
23 test \<^theory> \<^term>\<open>10 * 20 :: real\<close>;
24 test \<^theory> \<^term>\<open>10 \<up> 20 :: real\<close>;
26 test \<^theory> \<^term>\<open>10 + 20 :: int\<close>;
27 test \<^theory> \<^term>\<open>10 - 20 :: int\<close>;
28 test \<^theory> \<^term>\<open>10 * 20 :: int\<close>;
30 test \<^theory> \<^term>\<open>10 + 20 :: nat\<close>;
31 test \<^theory> \<^term>\<open>10 - 20 :: nat\<close>;
32 test \<^theory> \<^term>\<open>10 * 20 :: nat\<close>;