From 8a5c5e4ae0cab0ab627c25ece59453a8e4bd4b64 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 12 May 2023 20:17:26 +0200
Subject: Cleanup the files of the HOL4 backend

---
 backends/hol4/testDivDefScript.sml | 87 --------------------------------------
 1 file changed, 87 deletions(-)
 delete mode 100644 backends/hol4/testDivDefScript.sml

(limited to 'backends/hol4/testDivDefScript.sml')

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