diff options
Diffstat (limited to 'tests/hashmap')
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index bd066dd0..a21338b5 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -187,8 +187,8 @@ let rec hash_map_allocate_slots_fwd_lem t slots n = end #pop-options -(**** new *) -/// Under proper conditions, [new] doesn't fail and returns an empty hash map. +(**** new_with_capacity *) +/// Under proper conditions, [new_with_capacity] doesn't fail and returns an empty hash map. val hash_map_new_with_capacity_fwd_lem (t : Type0) (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : @@ -229,6 +229,16 @@ let hash_map_new_with_capacity_fwd_lem (t : Type0) (capacity : usize) end #pop-options +(**** new *) +/// [new] doesn't fail and returns an empty hash map. +val hash_map_new_fwd_lem (t : Type0) : + Lemma + (ensures ( + match hash_map_new_fwd t with + | Fail -> False + | Return hm -> hash_map_t_inv hm [])) + +let hash_map_new_fwd_lem t = hash_map_new_with_capacity_fwd_lem t 32 4 5 (**** clear_slots *) |