summaryrefslogtreecommitdiff
path: root/tests/lean/Hashmap
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Hashmap')
-rw-r--r--tests/lean/Hashmap/Funs.lean36
1 files changed, 18 insertions, 18 deletions
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index d7ac3b05..612e1848 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -400,38 +400,38 @@ 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 ¬ (i = 18#u64)
- then Result.fail .panic
- else
+ if i = 18#u64
+ then
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 ¬ (i1 = 56#u64)
- then Result.fail .panic
- else
+ if i1 = 56#u64
+ then
do
let (x, hm6) ← HashMap.remove U64 hm5 1024#usize
match x with
| none => Result.fail .panic
| some x1 =>
- if ¬ (x1 = 56#u64)
- then Result.fail .panic
- else
+ if x1 = 56#u64
+ then
do
let i2 ← HashMap.get U64 hm6 0#usize
- if ¬ (i2 = 42#u64)
- then Result.fail .panic
- else
+ if i2 = 42#u64
+ then
do
let i3 ← HashMap.get U64 hm6 128#usize
- if ¬ (i3 = 18#u64)
- then Result.fail .panic
- else
+ if i3 = 18#u64
+ then
do
let i4 ← HashMap.get U64 hm6 1056#usize
- if ¬ (i4 = 256#u64)
- then Result.fail .panic
- else Result.ok ()
+ if i4 = 256#u64
+ then Result.ok ()
+ else Result.fail .panic
+ else Result.fail .panic
+ else Result.fail .panic
+ else Result.fail .panic
+ else Result.fail .panic
+ else Result.fail .panic
end hashmap