summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-02-01 00:13:16 +0100
committerSon HO2023-06-04 21:54:38 +0200
commit26309503ab0d7710f03333d7762e484be94767e0 (patch)
tree573be1ce11529c620f7598c74238e3aa52a46aeb /backends
parent49903e84b1193565baa04a25864d6e54fed6f1de (diff)
Make minor modifications
Diffstat (limited to '')
-rw-r--r--backends/hol4/divDefLib.sml26
1 files changed, 26 insertions, 0 deletions
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index 08c8b91a..3ecb32df 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -1213,6 +1213,32 @@ val def_qt = ‘
val even_def = DefineDiv def_qt
+(* Complexigying the above definition *)
+val def_qt = ‘
+ (even (i : int) : bool result =
+ if i = 0 then
+ do
+ b <- Return T;
+ Return b
+ od
+ else do
+ b <- odd (i - 1);
+ Return b
+ od
+ ) /\
+ (odd (i : int) : bool result =
+ if i = 0 then
+ do
+ b <- Return F;
+ Return b
+ od
+ else do
+ b <- even (i - 1);
+ Return b
+ od)
+’
+
+val even_def = DefineDiv def_qt
Datatype:
list_t =