From 63ee3b1bc65b67aeed843f052d7f67c9f3c0ab89 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Feb 2024 23:16:57 +0100
Subject: Start fixing the tests

---
 tests/lean/NoNestedBorrows.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 0dd29429..bed71d94 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -139,12 +139,12 @@ def mix_arith_i32 (x : I32) (y : I32) (z : I32) : Result I32 :=
 /- [no_nested_borrows::CONST0]
    Source: 'src/no_nested_borrows.rs', lines 125:0-125:23 -/
 def const0_body : Result Usize := 1#usize + 1#usize
-def const0_c : Usize := eval_global const0_body (by simp)
+def const0_c : Usize := eval_global const0_body (by decide)
 
 /- [no_nested_borrows::CONST1]
    Source: 'src/no_nested_borrows.rs', lines 126:0-126:23 -/
 def const1_body : Result Usize := 2#usize * 2#usize
-def const1_c : Usize := eval_global const1_body (by simp)
+def const1_c : Usize := eval_global const1_body (by decide)
 
 /- [no_nested_borrows::cast_u32_to_i32]:
    Source: 'src/no_nested_borrows.rs', lines 128:0-128:37 -/
-- 
cgit v1.2.3