diff options
Diffstat (limited to 'tests/lean/misc-polonius_list/PoloniusList.lean')
| -rw-r--r-- | tests/lean/misc-polonius_list/PoloniusList.lean | 31 |
1 files changed, 0 insertions, 31 deletions
diff --git a/tests/lean/misc-polonius_list/PoloniusList.lean b/tests/lean/misc-polonius_list/PoloniusList.lean deleted file mode 100644 index 79696996..00000000 --- a/tests/lean/misc-polonius_list/PoloniusList.lean +++ /dev/null @@ -1,31 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [polonius_list] -import Base.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] -/ -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 h: 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] -/ -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 h: 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 - |