summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/misc')
-rw-r--r--tests/coq/misc/PoloniusList.v41
-rw-r--r--tests/coq/misc/_CoqProject3
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