diff options
Diffstat (limited to 'tests/coq/hashmap')
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 34 | ||||
| -rw-r--r-- | tests/coq/hashmap/_CoqProject | 4 |
2 files changed, 19 insertions, 19 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 04df873a..02aa0269 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -523,35 +523,35 @@ Definition test1 (n : nat) : result unit := hm3 <- hashMap_insert u64 n hm2 1024%usize 138%u64; hm4 <- hashMap_insert u64 n hm3 1056%usize 256%u64; i <- hashMap_get u64 n hm4 128%usize; - if negb (i s= 18%u64) - then Fail_ Failure - else ( + if i s= 18%u64 + then ( p <- hashMap_get_mut u64 n hm4 1024%usize; let (_, get_mut_back) := p in hm5 <- get_mut_back 56%u64; i1 <- hashMap_get u64 n hm5 1024%usize; - if negb (i1 s= 56%u64) - then Fail_ Failure - else ( + if i1 s= 56%u64 + then ( p1 <- hashMap_remove u64 n hm5 1024%usize; let (x, hm6) := p1 in match x with | None => Fail_ Failure | Some x1 => - if negb (x1 s= 56%u64) - then Fail_ Failure - else ( + if x1 s= 56%u64 + then ( i2 <- hashMap_get u64 n hm6 0%usize; - if negb (i2 s= 42%u64) - then Fail_ Failure - else ( + if i2 s= 42%u64 + then ( i3 <- hashMap_get u64 n hm6 128%usize; - if negb (i3 s= 18%u64) - then Fail_ Failure - else ( + if i3 s= 18%u64 + then ( i4 <- hashMap_get u64 n hm6 1056%usize; - if negb (i4 s= 256%u64) then Fail_ Failure else Ok tt))) - end)) + if i4 s= 256%u64 then Ok tt else Fail_ Failure) + else Fail_ Failure) + else Fail_ Failure) + else Fail_ Failure + end) + else Fail_ Failure) + else Fail_ Failure . End Hashmap_Funs. diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject index 7f80afbf..5d98662a 100644 --- a/tests/coq/hashmap/_CoqProject +++ b/tests/coq/hashmap/_CoqProject @@ -3,6 +3,6 @@ -arg -w -arg all -Hashmap_Types.v +Hashmap_Funs.v +Hashmap_Types.v Primitives.v -Hashmap_Funs.v |