diff options
Diffstat (limited to 'tests/lean/misc-polonius_list/PoloniusList.lean')
| -rw-r--r-- | tests/lean/misc-polonius_list/PoloniusList.lean | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tests/lean/misc-polonius_list/PoloniusList.lean b/tests/lean/misc-polonius_list/PoloniusList.lean index d679230d..a3bbfd0a 100644 --- a/tests/lean/misc-polonius_list/PoloniusList.lean +++ b/tests/lean/misc-polonius_list/PoloniusList.lean @@ -6,18 +6,18 @@ structure OpaqueDefs where /- [polonius_list::List] -/ inductive list_t (T : Type) := - | ListCons : T -> list_t T -> list_t T - | ListNil : list_t T + | 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 UInt32) (x : UInt32) : Result (list_t UInt32) := match h: ls with - | list_t.ListCons hd tl => + | list_t.Cons hd tl => if h: hd = x - then Result.ret (list_t.ListCons hd tl) + then Result.ret (list_t.Cons hd tl) else get_list_at_x_fwd tl x - | list_t.ListNil => Result.ret list_t.ListNil + | list_t.Nil => Result.ret list_t.Nil /- [polonius_list::get_list_at_x] -/ def get_list_at_x_back @@ -25,12 +25,12 @@ structure OpaqueDefs where Result (list_t UInt32) := match h: ls with - | list_t.ListCons hd tl => + | 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.ListCons hd tl0) - | list_t.ListNil => Result.ret ret0 + Result.ret (list_t.Cons hd tl0) + | list_t.Nil => Result.ret ret0 |