diff options
| author | Zyad Hassan | 2024-02-23 16:37:58 -0800 |
|---|---|---|
| committer | Son Ho | 2024-03-08 09:45:57 +0100 |
| commit | 5427563a8000f281ac614a2501fb9983beb44f21 (patch) | |
| tree | 55835ec19c84d06fb291cf3df456a90f88f8dc7e /tests/lean | |
| parent | 44248ccfe3bfb8c45e5bb434d8dfb3dfa6e6b69c (diff) | |
Fix tuple indexing for Lean backend
Diffstat (limited to 'tests/lean')
| -rw-r--r-- | tests/lean/NoNestedBorrows.lean | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 71d064d8..a326bdf7 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -643,7 +643,7 @@ def Tuple (T1 T2 : Type) := T1 × T2 /- [no_nested_borrows::use_tuple_struct]: Source: 'src/no_nested_borrows.rs', lines 556:0-556:48 -/ def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) := - Result.ret (1#u32, x.1) + Result.ret (1#u32, x.2) /- [no_nested_borrows::create_tuple_struct]: Source: 'src/no_nested_borrows.rs', lines 560:0-560:61 -/ |