From 26309503ab0d7710f03333d7762e484be94767e0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 1 Feb 2023 00:13:16 +0100
Subject: Make minor modifications

---
 backends/hol4/divDefLib.sml | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

(limited to 'backends')

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 =
-- 
cgit v1.2.3