diff options
author | Son Ho | 2023-03-08 00:39:05 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | 14aed083b850c2d8a77cfe394827aeecce06514b (patch) | |
tree | 8486ce9eb6ca80668d34c3422ef89e29018ec269 /tests/lean/misc-polonius_list | |
parent | c00d77052e8cb778e5311a4344cf8449dd3726b6 (diff) |
Improve the generation of variant names for Lean
Diffstat (limited to 'tests/lean/misc-polonius_list')
-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 |