diff options
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 20 |
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' -> |