1 files changed, 29 insertions, 0 deletions
diff --git a/backends/hol4/divDefLibExampleScript.sml b/backends/hol4/divDefLibExampleScript.sml
new file mode 100644
index 00000000..c4a57783
--- /dev/null
+++ b/backends/hol4/divDefLibExampleScript.sml
@@ -0,0 +1,29 @@
+(* Examples which use divDefLib.DefineDiv *)
+
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
+
+open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+open primitivesLib
+open divDefTheory divDefLib
+
+val [even_def, odd_def] = DefineDiv ‘
+  (even (i : int) : bool result =
+    if i = 0 then Return T else odd (i - 1)) /\
+  (odd (i : int) : bool result =
+    if i = 0 then Return F else even (i - 1))
+’
+
+val [nth_def] = DefineDiv ‘
+  nth (ls : 't list_t) (i : u32) : 't result =
+    case ls of
+    | ListCons x tl =>
+      if u32_to_int i = (0:int)
+      then (Return x)
+      else
+        do
+        i0 <- u32_sub i (int_to_u32 1);
+        nth tl i0
+        od
+    | ListNil => Fail Failure
+’