summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
authorSon Ho2023-11-08 14:28:44 +0100
committerSon Ho2023-11-08 14:28:44 +0100
commit530a5ae56209061f091bbcafee82de07039a8124 (patch)
tree6a82c5b7d34d734d83da1892f4fbb9a36cffec12 /tests/lean
parenta745e81c9949f24878f788fffd36667739c59330 (diff)
Update the Makefile and regenerate some tests
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/NoNestedBorrows.lean12
1 files changed, 12 insertions, 0 deletions
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