From a7452421be018e5d75065e2038f2f50042a80f3c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 10:42:10 +0100
Subject: Update the code generated for tuple projectors

---
 tests/lean/NoNestedBorrows.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/lean')

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index a326bdf7..a85209ea 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.2)
+  Result.ret (1#u32, x.#1)
 
 /- [no_nested_borrows::create_tuple_struct]:
    Source: 'src/no_nested_borrows.rs', lines 560:0-560:61 -/
-- 
cgit v1.2.3