diff options
Diffstat (limited to 'tests/lean/Paper.lean')
-rw-r--r-- | tests/lean/Paper.lean | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index dbd56f3e..03b96903 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -15,9 +15,9 @@ def ref_incr (x : I32) : Result I32 := def test_incr : Result Unit := do let x ← ref_incr 0#i32 - if ¬ (x = 1#i32) - then Result.fail .panic - else Result.ok () + if x = 1#i32 + then Result.ok () + else Result.fail .panic /- Unit test for [paper::test_incr] -/ #assert (test_incr == Result.ok ()) @@ -40,16 +40,16 @@ def test_choose : Result Unit := do let (z, choose_back) ← choose I32 true 0#i32 0#i32 let z1 ← z + 1#i32 - if ¬ (z1 = 1#i32) - then Result.fail .panic - else + if z1 = 1#i32 + then do let (x, y) ← choose_back z1 - if ¬ (x = 1#i32) - then Result.fail .panic - else if ¬ (y = 0#i32) - then Result.fail .panic - else Result.ok () + if x = 1#i32 + then if y = 0#i32 + then Result.ok () + else Result.fail .panic + else Result.fail .panic + else Result.fail .panic /- Unit test for [paper::test_choose] -/ #assert (test_choose == Result.ok ()) @@ -101,9 +101,9 @@ def test_nth : Result Unit := let x1 ← x + 1#i32 let l2 ← list_nth_mut_back x1 let i ← sum l2 - if ¬ (i = 7#i32) - then Result.fail .panic - else Result.ok () + if i = 7#i32 + then Result.ok () + else Result.fail .panic /- Unit test for [paper::test_nth] -/ #assert (test_nth == Result.ok ()) |