Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/ProgLang/calculate.sml
author wneuper <Walther.Neuper@jku.at>
Fri, 05 Aug 2022 08:45:37 +0200
changeset 60516 795d1352493a
parent 60509 2e0b7ca391dc
permissions -rw-r--r--
finish Calc_Binop, add signature EXAMPLE 
     1 (* Title:  "ProgLang/calculate.sml"

     2    Author: Walther Neuper 2021

     3    (c) copyright due to lincense terms.

     4 *)

     5 

     6 "-----------------------------------------------------------------------------------------------";

     7 "table of contents -----------------------------------------------------------------------------";

     8 "-----------------------------------------------------------------------------------------------";

     9 "----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";

    10 "-----------------------------------------------------------------------------------------------";

    11 "-----------------------------------------------------------------------------------------------";

    12 "-----------------------------------------------------------------------------------------------";

    13 

    14 "----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";

    15 "----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";

    16 "----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";

    17 

    18 fun test thy t = 

    19   writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, Calc_Binop.simplify @{context} t)));

    20 

    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>;

    25 

    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>;

    29 

    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>;
wneuper/isa