diff options
Diffstat (limited to 'tests/lean/NoNestedBorrows.lean')
-rw-r--r-- | tests/lean/NoNestedBorrows.lean | 8 |
1 files changed, 2 insertions, 6 deletions
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 -/ |