Merge pull request #82 from AeneasVerif/son/switch

Improve tuple projections and matches over integers in Lean

1 files changed, 6 insertions, 6 deletions

diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 3978bfc7..f0706725 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -397,14 +397,14 @@ def test1 : Result Unit :=
   let hm3 ← HashMap.insert U64 hm2 1024#usize 138#u64
   let hm4 ← HashMap.insert U64 hm3 1056#usize 256#u64
   let i ← HashMap.get U64 hm4 128#usize
-  if not (i = 18#u64)
+  if ¬ (i = 18#u64)
   then Result.fail .panic
   else
     do
     let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024#usize
     let hm5 ← get_mut_back 56#u64
     let i1 ← HashMap.get U64 hm5 1024#usize
-    if not (i1 = 56#u64)
+    if ¬ (i1 = 56#u64)
     then Result.fail .panic
     else
       do
@@ -412,22 +412,22 @@ def test1 : Result Unit :=
       match x with
       | none => Result.fail .panic
       | some x1 =>
-        if not (x1 = 56#u64)
+        if ¬ (x1 = 56#u64)
         then Result.fail .panic
         else
           do
           let i2 ← HashMap.get U64 hm6 0#usize
-          if not (i2 = 42#u64)
+          if ¬ (i2 = 42#u64)
           then Result.fail .panic
           else
             do
             let i3 ← HashMap.get U64 hm6 128#usize
-            if not (i3 = 18#u64)
+            if ¬ (i3 = 18#u64)
             then Result.fail .panic
             else
               do
               let i4 ← HashMap.get U64 hm6 1056#usize
-              if not (i4 = 256#u64)
+              if ¬ (i4 = 256#u64)
               then Result.fail .panic
               else Result.ret ()