summaryrefslogtreecommitdiff
path: root/tests/hashmap
diff options
context:
space:
mode:
authorSon Ho2022-02-12 11:53:57 +0100
committerSon Ho2022-02-12 11:53:57 +0100
commitd2030538caf01bac4aa06c312bd4d8b1cbd3c6ea (patch)
tree3934cef7c8e5936a04cedad0ff03fd8d657fc84e /tests/hashmap
parent527c55e1182fe14c5615b219c896266129419e19 (diff)
Make minor modifications to Hashmap.Properties.fst
Diffstat (limited to 'tests/hashmap')
-rw-r--r--tests/hashmap/Hashmap.Properties.fst20
1 files changed, 12 insertions, 8 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 577398fd..a27ee34a 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -1391,16 +1391,20 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' =
(*** move_elements_from_list *)
-type hash_map_slots_s_res (t : Type0) = res:result (hash_map_slots_s t){
- match res with
- | Fail -> True
- | Return hm -> is_pos_usize (length hm)
- }
-
let rec hash_map_move_elements_from_list_s
- (#t : Type0) (hm : hash_map_slots_s t{is_pos_usize (length hm)})
+ (#t : Type0) (hm : hash_map_slots_s_nes t)
(ls : slot_s t) :
- Tot (hash_map_slots_s_res t) (decreases ls) =
+ Pure (result (hash_map_slots_s t))
+ (requires (True))
+ (ensures (fun res ->
+ // Having a great time here: if we use `result (hash_map_slots_s_res t)`
+ // as the return type, instead of having this awkward match, the proof
+ // of [hash_map_move_elements_fwd_back_lem] fails. I guess it comes from
+ // F*'s poor subtyping.
+ match res with
+ | Fail -> True
+ | Return hm -> is_pos_usize (length hm)))
+ (decreases ls) =
match ls with
| [] -> Return hm
| (key, value) :: ls' ->