summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2022-02-14 11:52:09 +0100
committerSon Ho2022-02-14 11:52:09 +0100
commitc9fd7cd50fd8ed08808bb3a682baddd525c4c448 (patch)
tree00ff676c9086b012c82bb74517c40fe8cb366fd3 /tests
parent7b4e45d1dd9b88d4f5b147659577e495ca50f8fd (diff)
Make minor modifications
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Hashmap.Properties.fsti7
1 files changed, 4 insertions, 3 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fsti b/tests/hashmap/Hashmap.Properties.fsti
index 60df42ac..80c0de06 100644
--- a/tests/hashmap/Hashmap.Properties.fsti
+++ b/tests/hashmap/Hashmap.Properties.fsti
@@ -30,10 +30,11 @@ val find_s (#t : Type0) (hm : hash_map_t t) (k : key) : option t
/// whenever we reach the max load, unless we can't resize anymore because
/// there are already too many entries. This way, we maintain performance by
/// limiting the hash collisions.
-/// This is embodied by the following property, which is maintained by the
-/// invariant.
+/// This is expressed by the following property, which is maintained in the hash
+/// map invariant.
val hash_map_not_overloaded_lem (#t : Type0) (hm : hash_map_t t) :
- Lemma (requires (hash_map_t_inv hm))
+ Lemma
+ (requires (hash_map_t_inv hm))
(ensures (
// The capacity is the number of slots
let capacity = length hm.hash_map_slots in