diff options
| author | Son Ho | 2023-09-07 16:06:14 +0200 |
|---|---|---|
| committer | Son Ho | 2023-09-07 16:06:14 +0200 |
| commit | ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 (patch) | |
| tree | 933d2bd806026930d216e4f16f113ea2749ca250 /tests/hol4/hashmap/hashmap_PropertiesScript.sml | |
| parent | 1181aecddbcb3232c21b191fbde59c2e9596846a (diff) | |
Regenerate the test files and fix a proof
Diffstat (limited to '')
| -rw-r--r-- | tests/hol4/hashmap/hashmap_PropertiesScript.sml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml index 7259f2f5..8bc12fa5 100644 --- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml +++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml @@ -1296,7 +1296,7 @@ Proof rw [hash_map_try_resize_fwd_back_def] >> (* “_ <-- mk_usize (u32_to_int core_num_u32_max_c)” *) assume_tac usize_u32_bounds >> - fs [core_num_u32_max_c_def, core_num_u32_max_body_def, get_return_value_def, u32_max_def] >> + fs [core_u32_max_def, u32_max_def] >> massage >> fs [mk_usize_def, u32_max_def] >> (* / 2 *) progress >> |