1 files changed, 0 insertions, 87 deletions
diff --git a/backends/hol4/testDivDefScript.sml b/backends/hol4/testDivDefScript.sml
deleted file mode 100644
index 4a87895f..00000000
--- a/backends/hol4/testDivDefScript.sml
+++ /dev/null
@@ -1,87 +0,0 @@
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib divDefLib
-
-val _ = new_theory "testDivDef"
-
-val def_qt = ‘
-  (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 even_def = DefineDiv def_qt
-
-(* Complexifying the above definition, and overriding on purpose *)
-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 =
-    ListCons 't list_t
-  | ListNil
-End
-
-val def_qt = ‘
-  nth_mut_fwd (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_mut_fwd tl i0
-      od
-  | ListNil =>
-    Fail Failure
-’
-
-val nth_mut_fwd_def = DefineDiv def_qt
-
-(* Complexifying the above definition, and overriding on purpose *)
-val def_qt = ‘
-  nth_mut_fwd (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);
-      x <- nth_mut_fwd tl i0;
-      Return x
-      od
-  | ListNil => 
-    Fail Failure
-’
-
-val nth_mut_fwd_def = DefineDiv def_qt
-
-val _ = export_theory ()