summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-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 =