Merge branch 'son/clean' into checked-ops

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