diff options
author | Son Ho | 2023-05-09 10:40:19 +0200 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | 50d1542f830b7ceb73efd34573b6b56b4971a114 (patch) | |
tree | c73b6c415b39cdbc3d92ec3056a2521445ff8afc /tests/lean/misc-polonius_list/PoloniusList.lean | |
parent | 4078f2569b362920a648622be73761cddde8a288 (diff) |
Regenerate the translated files for Lean
Diffstat (limited to 'tests/lean/misc-polonius_list/PoloniusList.lean')
-rw-r--r-- | tests/lean/misc-polonius_list/PoloniusList.lean | 59 |
1 files changed, 27 insertions, 32 deletions
diff --git a/tests/lean/misc-polonius_list/PoloniusList.lean b/tests/lean/misc-polonius_list/PoloniusList.lean index a3bbfd0a..79696996 100644 --- a/tests/lean/misc-polonius_list/PoloniusList.lean +++ b/tests/lean/misc-polonius_list/PoloniusList.lean @@ -2,35 +2,30 @@ -- [polonius_list] import Base.Primitives -structure OpaqueDefs where - - /- [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 UInt32) (x : UInt32) : Result (list_t UInt32) := - 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 UInt32) (x : UInt32) (ret0 : list_t UInt32) : - Result (list_t UInt32) - := - 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 - +/- [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 + |