summaryrefslogtreecommitdiff
path: root/tests/lean/Paper.lean
diff options
context:
space:
mode:
authorSon Ho2024-03-08 08:03:48 +0100
committerSon Ho2024-03-08 08:03:48 +0100
commitf74647773d7dd21580fd938dd9b4e300719b0234 (patch)
tree397fa643ef5d372b65cada410937c0030002a340 /tests/lean/Paper.lean
parente1e888f23935bfb34830fe160593e09df75a7f20 (diff)
Regenerate the test files
Diffstat (limited to '')
-rw-r--r--tests/lean/Paper.lean10
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index a35c8db0..4930a05c 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -15,7 +15,7 @@ def ref_incr (x : I32) : Result I32 :=
def test_incr : Result Unit :=
do
let i ← ref_incr 0#i32
- if not (i = 1#i32)
+ if ¬ (i = 1#i32)
then Result.fail .panic
else Result.ret ()
@@ -40,14 +40,14 @@ def test_choose : Result Unit :=
do
let (z, choose_back) ← choose I32 true 0#i32 0#i32
let z1 ← z + 1#i32
- if not (z1 = 1#i32)
+ if ¬ (z1 = 1#i32)
then Result.fail .panic
else
do
let (x, y) ← choose_back z1
- if not (x = 1#i32)
+ if ¬ (x = 1#i32)
then Result.fail .panic
- else if not (y = 0#i32)
+ else if ¬ (y = 0#i32)
then Result.fail .panic
else Result.ret ()
@@ -101,7 +101,7 @@ def test_nth : Result Unit :=
let x1 ← x + 1#i32
let l2 ← list_nth_mut_back x1
let i ← sum l2
- if not (i = 7#i32)
+ if ¬ (i = 7#i32)
then Result.fail .panic
else Result.ret ()