diff options
| author | Son Ho | 2024-03-08 08:03:48 +0100 | 
|---|---|---|
| committer | Son Ho | 2024-03-08 08:03:48 +0100 | 
| commit | f74647773d7dd21580fd938dd9b4e300719b0234 (patch) | |
| tree | 397fa643ef5d372b65cada410937c0030002a340 /tests/lean/Paper.lean | |
| parent | e1e888f23935bfb34830fe160593e09df75a7f20 (diff) | |
Regenerate the test files
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/Paper.lean | 10 | 
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 ()  | 
