From 3adbe18d36df3767e98f30b760ccd9c6ace640ad Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 17:01:16 +0200
Subject: Rename some subdirectories for consistency

---
 tests/hol4/polonius_list/poloniusListScript.sml | 37 +++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 tests/hol4/polonius_list/poloniusListScript.sml

(limited to 'tests/hol4/polonius_list/poloniusListScript.sml')

diff --git a/tests/hol4/polonius_list/poloniusListScript.sml b/tests/hol4/polonius_list/poloniusListScript.sml
new file mode 100644
index 00000000..06876ed4
--- /dev/null
+++ b/tests/hol4/polonius_list/poloniusListScript.sml
@@ -0,0 +1,37 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [polonius_list] *)
+open primitivesLib divDefLib
+
+val _ = new_theory "poloniusList"
+
+
+Datatype:
+  (** [polonius_list::List] *)
+  list_t = | ListCons 't list_t | ListNil
+End
+
+val [get_list_at_x_fwd_def] = DefineDiv ‘
+  (** [polonius_list::get_list_at_x]: forward function *)
+  get_list_at_x_fwd (ls : u32 list_t) (x : u32) : u32 list_t result =
+    (case ls of
+    | ListCons hd tl =>
+      if hd = x then Return (ListCons hd tl) else get_list_at_x_fwd tl x
+    | ListNil => Return ListNil)
+’
+
+val [get_list_at_x_back_def] = DefineDiv ‘
+  (** [polonius_list::get_list_at_x]: backward function 0 *)
+  get_list_at_x_back
+    (ls : u32 list_t) (x : u32) (ret : u32 list_t) : u32 list_t result =
+    (case ls of
+    | ListCons hd tl =>
+      if hd = x
+      then Return ret
+      else (do
+            tl0 <- get_list_at_x_back tl x ret;
+            Return (ListCons hd tl0)
+            od)
+    | ListNil => Return ret)
+’
+
+val _ = export_theory ()
-- 
cgit v1.2.3