diff options
Diffstat (limited to 'tests/lean/PoloniusList.lean')
-rw-r--r-- | tests/lean/PoloniusList.lean | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean new file mode 100644 index 00000000..671f54ea --- /dev/null +++ b/tests/lean/PoloniusList.lean @@ -0,0 +1,33 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [polonius_list] +import Base +open Primitives + +/- [polonius_list::List] -/ +inductive list_t (T : Type) := +| Cons : T -> list_t T -> list_t T +| Nil : list_t T + +/- [polonius_list::get_list_at_x] -/ +divergent def get_list_at_x_fwd + (ls : list_t U32) (x : U32) : Result (list_t U32) := + match h: ls with + | list_t.Cons hd tl => + if hd = x + then Result.ret (list_t.Cons hd tl) + else get_list_at_x_fwd tl x + | list_t.Nil => Result.ret list_t.Nil + +/- [polonius_list::get_list_at_x] -/ +divergent def get_list_at_x_back + (ls : list_t U32) (x : U32) (ret0 : list_t U32) : Result (list_t U32) := + match h: ls with + | list_t.Cons hd tl => + if hd = x + then Result.ret ret0 + else + do + let tl0 ← get_list_at_x_back tl x ret0 + Result.ret (list_t.Cons hd tl0) + | list_t.Nil => Result.ret ret0 + |