summaryrefslogtreecommitdiff
path: root/tests/hol4/hashmap
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/hashmap')
-rw-r--r--tests/hol4/hashmap/hashmap_PropertiesScript.sml6
1 files changed, 5 insertions, 1 deletions
diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index 68ed2d4e..6b64affe 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -203,7 +203,11 @@ Definition hash_map_t_base_inv_def:
)
End
-(* The invariant that we reveal to the user *)
+(* The invariant that we reveal to the user.
+
+ The conditions about the hash map load factor are a overkill, but we
+ want to see how the non-linear arithmetic proofs go.
+ *)
Definition hash_map_t_inv_def:
hash_map_t_inv (hm : 't hash_map_t) : bool = (
(* Base invariant *)