diff options
Diffstat (limited to 'tests/hol4/hashmap')
| -rw-r--r-- | tests/hol4/hashmap/hashmap_PropertiesScript.sml | 6 |
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 *) |