diff options
author | Son Ho | 2023-07-04 18:09:36 +0200 |
---|---|---|
committer | Son Ho | 2023-07-04 18:09:36 +0200 |
commit | b643bd00747e75d69b6066c55a1798b61277c4b6 (patch) | |
tree | 84bbebe82964efc0d779ea782f3ae4b946ca3483 /tests/lean/PoloniusList.lean | |
parent | 74b3ce71b0e3794853aa1413afaaaa05c8cc5a84 (diff) |
Regenerate the Lean test files
Diffstat (limited to '')
-rw-r--r-- | tests/lean/PoloniusList.lean | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean index 671f54ea..0f2a05e3 100644 --- a/tests/lean/PoloniusList.lean +++ b/tests/lean/PoloniusList.lean @@ -3,15 +3,17 @@ import Base open Primitives +namespace PoloniusList + /- [polonius_list::List] -/ inductive list_t (T : Type) := -| Cons : T -> list_t T -> list_t T +| Cons : T → list_t T → list_t T | Nil : list_t T /- [polonius_list::get_list_at_x] -/ divergent def get_list_at_x_fwd (ls : list_t U32) (x : U32) : Result (list_t U32) := - match h: ls with + match ls with | list_t.Cons hd tl => if hd = x then Result.ret (list_t.Cons hd tl) @@ -21,7 +23,7 @@ divergent def get_list_at_x_fwd /- [polonius_list::get_list_at_x] -/ divergent def get_list_at_x_back (ls : list_t U32) (x : U32) (ret0 : list_t U32) : Result (list_t U32) := - match h: ls with + match ls with | list_t.Cons hd tl => if hd = x then Result.ret ret0 @@ -31,3 +33,4 @@ divergent def get_list_at_x_back Result.ret (list_t.Cons hd tl0) | list_t.Nil => Result.ret ret0 +end PoloniusList |