Merge pull request #46 from AeneasVerif/son_improves

Minor improvements for the extraction

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