From b455f94c841b2423898f39bc9b6a4c35a3db56e3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 16:20:20 +0200
Subject: Regenerate the test files

---
 tests/lean/PoloniusList.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tests/lean/PoloniusList.lean')

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
-- 
cgit v1.2.3