summaryrefslogtreecommitdiff
path: root/tests/lean/PoloniusList.lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/PoloniusList.lean10
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 59c557a0..09f41056 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -20,16 +20,16 @@ divergent def get_list_at_x
match ls with
| List.Cons hd tl =>
if hd = x
- then Result.ret (List.Cons hd tl, Result.ret)
+ then Result.ok (List.Cons hd tl, Result.ok)
else
do
let (l, get_list_at_x_back) ← get_list_at_x tl x
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← get_list_at_x_back ret
- Result.ret (List.Cons hd tl1)
- Result.ret (l, back_'a)
- | List.Nil => Result.ret (List.Nil, Result.ret)
+ Result.ok (List.Cons hd tl1)
+ Result.ok (l, back)
+ | List.Nil => Result.ok (List.Nil, Result.ok)
end polonius_list