From b6676f6dc3b1471317cce8e04e9cb7203168f75c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 11 Nov 2022 16:05:56 +0100
Subject: Make minor modifications to the tests and regenerate the .fst files

---
 tests/misc/PoloniusList.fst | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 tests/misc/PoloniusList.fst

(limited to 'tests/misc/PoloniusList.fst')

diff --git a/tests/misc/PoloniusList.fst b/tests/misc/PoloniusList.fst
new file mode 100644
index 00000000..73e98884
--- /dev/null
+++ b/tests/misc/PoloniusList.fst
@@ -0,0 +1,41 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [polonius_list] *)
+module PoloniusList
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [polonius_list::List] *)
+type list_t (t : Type0) =
+| ListCons : t -> list_t t -> list_t t
+| ListNil : list_t t
+
+(** [polonius_list::get_list_at_x] *)
+let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
+  begin match ls with
+  | ListCons hd tl ->
+    if hd = x
+    then Return (ListCons hd tl)
+    else
+      begin match get_list_at_x_fwd tl x with
+      | Fail -> Fail
+      | Return l -> Return l
+      end
+  | ListNil -> Return ListNil
+  end
+
+(** [polonius_list::get_list_at_x] *)
+let rec get_list_at_x_back
+  (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
+  begin match ls with
+  | ListCons hd tl ->
+    if hd = x
+    then Return ret
+    else
+      begin match get_list_at_x_back tl x ret with
+      | Fail -> Fail
+      | Return tl0 -> Return (ListCons hd tl0)
+      end
+  | ListNil -> Return ret
+  end
+
-- 
cgit v1.2.3