From 5e99d127e0a746f5779779756fccf79f15c19d10 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 20 Mar 2024 06:17:41 +0100
Subject: Regenerate the code

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

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

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 2112e282..5f9ec0f2 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -487,9 +487,7 @@ def id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
   :=
-  let back_'a := fun ret => let (t, t1) := ret
-                            Result.ret (t, t1)
-  Result.ret ((x, y), back_'a)
+  Result.ret ((x, y), Result.ret)
 
 /- [no_nested_borrows::id_mut_pair2]:
    Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 -/
@@ -498,9 +496,7 @@ def id_mut_pair2
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
   :=
   let (t, t1) := p
-  let back_'a := fun ret => let (t2, t3) := ret
-                            Result.ret (t2, t3)
-  Result.ret ((t, t1), back_'a)
+  Result.ret ((t, t1), Result.ret)
 
 /- [no_nested_borrows::id_mut_pair3]:
    Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 -/
-- 
cgit v1.2.3