diff options
| author | Jonathan Protzenko | 2023-01-31 15:28:17 -0800 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | 7586cf83f59ca784ff4bfd5d11e460fd41acec98 (patch) | |
| tree | 7a023c2d7fcc8ee76e45568524c4dba1ea95f03d /tests/lean/hashmap_on_disk/HashmapMain | |
| parent | b30bac9e20735ab47327a2ac3122c2cfce162845 (diff) | |
Fill out more of the primitives file, attempt at type classes for scalar_cast
Diffstat (limited to 'tests/lean/hashmap_on_disk/HashmapMain')
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index f9d4a8c5..79d711e9 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -264,7 +264,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back def hashmap_hash_map_try_resize_fwd_back (T : Type) (self : hashmap_hash_map_t T) : result (hashmap_hash_map_t T) := do - let max_usize <- scalar_cast U32 Usize core_num_u32_max_c + let max_usize <- scalar_cast USize core_num_u32_max_c let capacity := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots let n1 <- USize.checked_div max_usize (USize.ofNatCore 2 (by intlit)) let (i, i0) := self.hashmap_hash_map_max_load_factor @@ -401,7 +401,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back result.ret (hashmap_list_t.HashmapListCons ckey cvalue l) | hashmap_list_t.HashmapListNil => result.fail error.panic - termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key => + termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 => hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key |