blob: 79696996f1ea5af881d8ca2744a0404f3f538a1b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
-- 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
|
