From dcd34ceed0c52738b1bb8139e7130db9bad1a774 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 10:22:51 +0100
Subject: Fix issues with the builtin names

---
 tests/lean/NoNestedBorrows.lean | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

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

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index c4a6a265..79049837 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -151,11 +151,13 @@ def test_list1 : Result Unit :=
 
 /- [no_nested_borrows::test_box1]: forward function -/
 def test_box1 : Result Unit :=
-  let b := 1#i32
-  let x := b
-  if not (x = 1#i32)
-  then Result.fail Error.panic
-  else Result.ret ()
+  do
+    let b := 0#i32
+    let b0 ← alloc.boxed.Box.deref_mut_back I32 b 1#i32
+    let x ← alloc.boxed.Box.deref I32 b0
+    if not (x = 1#i32)
+    then Result.fail Error.panic
+    else Result.ret ()
 
 /- Unit test for [no_nested_borrows::test_box1] -/
 #assert (test_box1 == .ret ())
-- 
cgit v1.2.3