Add a comment

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 *)