From 62699c2ebb2d10301f437ca06961a82c30913405 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 12 May 2023 20:54:54 +0200
Subject: Fix minor issues

---
 backends/hol4/divDefLibTestScript.sml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

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

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