Merge pull request #123 from AeneasVerif/son/clean

Cleanup the code in preparation of the nested loops

1 files changed, 4 insertions, 4 deletions

diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index c657237f..09f41056 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -20,7 +20,7 @@ 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
@@ -28,8 +28,8 @@ divergent def get_list_at_x
         fun ret =>
           do
           let tl1 ← get_list_at_x_back ret
-          Result.ret (List.Cons hd tl1)
-      Result.ret (l, back)
-  | 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