Fix minor issues

1 files changed, 8 insertions, 4 deletions

diff --git a/backends/hol4/divDefLibTestScript.sml b/backends/hol4/divDefLibTestScript.sml
index c4a57783..b1243065 100644
--- a/backends/hol4/divDefLibTestScript.sml
+++ b/backends/hol4/divDefLibTestScript.sml
@@ -8,12 +8,16 @@ 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))
+  (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))
 ’
 
+Datatype:
+  list_t =
+    ListCons 't list_t
+  | ListNil
+End
+
 val [nth_def] = DefineDiv ‘
   nth (ls : 't list_t) (i : u32) : 't result =
     case ls of