diff options
Diffstat (limited to 'tests/fstar/hashmap_on_disk')
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 22 |
1 files changed, 8 insertions, 14 deletions
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index cb8460c7..e8cd54c1 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -75,7 +75,7 @@ let hashmap_hash_map_clear_fwd_back let* v = hashmap_hash_map_clear_loop_fwd_back t self.hashmap_hash_map_slots 0 in Return - { self where hashmap_hash_map_num_entries = 0; hashmap_hash_map_slots = v } + { self with hashmap_hash_map_num_entries = 0; hashmap_hash_map_slots = v } (** [hashmap_main::hashmap::HashMap::{0}::len] *) let hashmap_hash_map_len_fwd @@ -145,17 +145,14 @@ let hashmap_hash_map_insert_no_resize_fwd_back vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in Return - { - self - where - hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v + { self with hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v } else let* l0 = hashmap_hash_map_insert_in_list_back t key value l in let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in - Return { self where hashmap_hash_map_slots = v } + Return { self with hashmap_hash_map_slots = v } (** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 @@ -228,11 +225,11 @@ let hashmap_hash_map_try_resize_fwd_back Return { ntable0 - where + with hashmap_hash_map_num_entries = self.hashmap_hash_map_num_entries; hashmap_hash_map_max_load_factor = (i, i0) } - else Return { self where hashmap_hash_map_max_load_factor = (i, i0) } + else Return { self with hashmap_hash_map_max_load_factor = (i, i0) } (** [hashmap_main::hashmap::HashMap::{0}::insert] *) let hashmap_hash_map_insert_fwd_back @@ -371,7 +368,7 @@ let hashmap_hash_map_get_mut_back let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in - Return { self where hashmap_hash_map_slots = v } + Return { self with hashmap_hash_map_slots = v } (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) let rec hashmap_hash_map_remove_from_list_loop_fwd @@ -463,7 +460,7 @@ let hashmap_hash_map_remove_back let* v = vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in - Return { self where hashmap_hash_map_slots = v } + Return { self with hashmap_hash_map_slots = v } | Some x0 -> let* i0 = usize_sub self.hashmap_hash_map_num_entries 1 in let* l0 = hashmap_hash_map_remove_from_list_back t key l in @@ -471,10 +468,7 @@ let hashmap_hash_map_remove_back vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod l0 in Return - { - self - where - hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v + { self with hashmap_hash_map_num_entries = i0; hashmap_hash_map_slots = v } end |