From 530a5ae56209061f091bbcafee82de07039a8124 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 8 Nov 2023 14:28:44 +0100
Subject: Update the Makefile and regenerate some tests

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

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

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index d6d603ce..c4a6a265 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -60,6 +60,18 @@ def div_test1 (x : U32) : Result U32 :=
 def rem_test (x : U32) (y : U32) : Result U32 :=
   x % y
 
+/- [no_nested_borrows::mul_test]: forward function -/
+def mul_test (x : U32) (y : U32) : Result U32 :=
+  x * y
+
+/- [no_nested_borrows::CONST0] -/
+def const0_body : Result Usize := 1#usize + 1#usize
+def const0_c : Usize := eval_global const0_body (by simp)
+
+/- [no_nested_borrows::CONST1] -/
+def const1_body : Result Usize := 2#usize * 2#usize
+def const1_c : Usize := eval_global const1_body (by simp)
+
 /- [no_nested_borrows::cast_test]: forward function -/
 def cast_test (x : U32) : Result I32 :=
   Scalar.cast .I32 x
-- 
cgit v1.2.3