diff options
author | Son Ho | 2023-11-21 10:22:51 +0100 |
---|---|---|
committer | Son Ho | 2023-11-21 10:22:51 +0100 |
commit | dcd34ceed0c52738b1bb8139e7130db9bad1a774 (patch) | |
tree | 50dae3ab70a5b22c5751d891893aff87e734d724 /tests | |
parent | db58a6bcc95c66febc70e90af928feae7dddf56c (diff) |
Fix issues with the builtin names
Diffstat (limited to 'tests')
-rw-r--r-- | tests/lean/NoNestedBorrows.lean | 12 |
1 files changed, 7 insertions, 5 deletions
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 ()) |