summaryrefslogtreecommitdiff
path: root/tests/lean/PoloniusList.lean
diff options
context:
space:
mode:
authorSon Ho2023-11-24 17:41:42 +0100
committerSon Ho2023-11-24 17:41:42 +0100
commitd84040e000333d6d2a212fb849a38fb73a65eb48 (patch)
treec15309842c8e37b533171e1f6e44a5362cbde292 /tests/lean/PoloniusList.lean
parent1c8187d7f4129e09f23d3b5caf33938a0c91ea77 (diff)
Regenerate the files
Diffstat (limited to '')
-rw-r--r--tests/lean/PoloniusList.lean8
1 files changed, 4 insertions, 4 deletions
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 0ef71791..37f0dffb 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -24,15 +24,15 @@ divergent def get_list_at_x (ls : List U32) (x : U32) : Result (List U32) :=
/- [polonius_list::get_list_at_x]: backward function 0
Source: 'src/polonius_list.rs', lines 13:0-13:76 -/
divergent def get_list_at_x_back
- (ls : List U32) (x : U32) (ret0 : List U32) : Result (List U32) :=
+ (ls : List U32) (x : U32) (ret : List U32) : Result (List U32) :=
match ls with
| List.Cons hd tl =>
if hd = x
- then Result.ret ret0
+ then Result.ret ret
else
do
- let tl0 ← get_list_at_x_back tl x ret0
+ let tl0 ← get_list_at_x_back tl x ret
Result.ret (List.Cons hd tl0)
- | List.Nil => Result.ret ret0
+ | List.Nil => Result.ret ret
end polonius_list