diff options
| author | Son Ho | 2023-12-05 17:34:13 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-05 17:34:13 +0100 |
| commit | 726db4911add81a853aafcec3936b457aaeff5b4 (patch) | |
| tree | 2663915767c3558203990ed14f8d5604b7fd21d1 /tests/hol4/hashmap/hashmap_FunsTheory.sig | |
| parent | 92887b89e35607e99bae2f19e4c5b2f162683d02 (diff) | |
| parent | 4795e5f823bc89504855d8eb946b111d9314f4d5 (diff) | |
Merge branch 'main' into son_fixes2
Diffstat (limited to 'tests/hol4/hashmap/hashmap_FunsTheory.sig')
| -rw-r--r-- | tests/hol4/hashmap/hashmap_FunsTheory.sig | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/tests/hol4/hashmap/hashmap_FunsTheory.sig b/tests/hol4/hashmap/hashmap_FunsTheory.sig index 50482547..bb3e192b 100644 --- a/tests/hol4/hashmap/hashmap_FunsTheory.sig +++ b/tests/hol4/hashmap/hashmap_FunsTheory.sig @@ -3,8 +3,6 @@ sig type thm = Thm.thm (* Definitions *) - val core_num_u32_max_body_def : thm - val core_num_u32_max_c_def : thm val hash_key_fwd_def : thm val hash_map_allocate_slots_fwd_def : thm val hash_map_allocate_slots_loop_fwd_def : thm @@ -48,14 +46,6 @@ sig (* [hashmap_Types] Parent theory of "hashmap_Funs" - [core_num_u32_max_body_def] Definition - - ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295) - - [core_num_u32_max_c_def] Definition - - ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body - [hash_key_fwd_def] Definition ⊢ ∀k. hash_key_fwd k = Return k @@ -472,7 +462,7 @@ sig ⊢ ∀self. hash_map_try_resize_fwd_back self = do - max_usize <- mk_usize (u32_to_int core_num_u32_max_c); + max_usize <- mk_usize (u32_to_int core_u32_max); capacity <<- vec_len self.hash_map_slots; n1 <- usize_div max_usize (int_to_usize 2); (i,i0) <<- self.hash_map_max_load_factor; |