From 3595f1c6174dbc356d024fcdf74aaef8b1fd533e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 1 Jun 2023 23:20:47 +0200
Subject: Add a comment

---
 tests/hol4/hashmap/hashmap_PropertiesScript.sml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'tests/hol4/hashmap')

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 *)
-- 
cgit v1.2.3