From 975ddb208f18cb4ba46293dd788c46eb1ce43938 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:58:44 +0200
Subject: Regenerate the test files

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

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

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 5f9ec0f2..b90f6aef 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -331,10 +331,10 @@ def choose
   Result (T × (T → Result (T × T)))
   :=
   if b
-  then let back_'a := fun ret => Result.ret (ret, y)
-       Result.ret (x, back_'a)
-  else let back_'a := fun ret => Result.ret (x, ret)
-       Result.ret (y, back_'a)
+  then let back := fun ret => Result.ret (ret, y)
+       Result.ret (x, back)
+  else let back := fun ret => Result.ret (x, ret)
+       Result.ret (y, back)
 
 /- [no_nested_borrows::choose_test]:
    Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 -/
@@ -406,18 +406,18 @@ divergent def list_nth_mut
   | List.Cons x tl =>
     if i = 0#u32
     then
-      let back_'a := fun ret => Result.ret (List.Cons ret tl)
-      Result.ret (x, back_'a)
+      let back := fun ret => Result.ret (List.Cons ret tl)
+      Result.ret (x, back)
     else
       do
       let i1 ← i - 1#u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← list_nth_mut_back ret
           Result.ret (List.Cons x tl1)
-      Result.ret (t, back_'a)
+      Result.ret (t, back)
   | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::list_rev_aux]:
-- 
cgit v1.2.3