2 files changed, 43 insertions, 1 deletions
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
new file mode 100644
index 00000000..6d6ea537
--- /dev/null
+++ b/tests/coq/misc/PoloniusList.v
@@ -0,0 +1,41 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [polonius_list] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module PoloniusList .
+
+(** [polonius_list::List] *)
+Inductive List_t (T : Type) :=
+| ListCons : T -> List_t T -> List_t T
+| ListNil : List_t T
+.
+
+Arguments ListCons {T} _ _  .
+Arguments ListNil {T}  .
+
+(** [polonius_list::get_list_at_x] *)
+Fixpoint get_list_at_x_fwd (ls : List_t u32) (x : u32) : result (List_t u32) :=
+  match ls with
+  | ListCons hd tl =>
+    if hd s= x
+    then Return (ListCons hd tl)
+    else (l <- get_list_at_x_fwd tl x; Return l)
+  | ListNil => Return ListNil
+  end
+  .
+
+(** [polonius_list::get_list_at_x] *)
+Fixpoint get_list_at_x_back
+  (ls : List_t u32) (x : u32) (ret : List_t u32) : result (List_t u32) :=
+  match ls with
+  | ListCons hd tl =>
+    if hd s= x
+    then Return ret
+    else (tl0 <- get_list_at_x_back tl x ret; Return (ListCons hd tl0))
+  | ListNil => Return ret
+  end
+  .
+
+End PoloniusList .
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 7f4981fa..16fcaf44 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -9,4 +9,5 @@ External__Funs.v
 External__Opaque.v
 External__Types.v
 NoNestedBorrows.v
-Paper.v
-\ No newline at end of file
+Paper.v
+PoloniusList.v
+\ No newline at end of file