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

---
 .../hol4/misc-polonius_list/poloniusListScript.sml | 37 ----------------------
 1 file changed, 37 deletions(-)
 delete mode 100644 tests/hol4/misc-polonius_list/poloniusListScript.sml

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

diff --git a/tests/hol4/misc-polonius_list/poloniusListScript.sml b/tests/hol4/misc-polonius_list/poloniusListScript.sml
deleted file mode 100644
index 06876ed4..00000000
--- a/tests/hol4/misc-polonius_list/poloniusListScript.sml
+++ /dev/null
@@ -1,37 +0,0 @@
-(** 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