diff options
author | Son Ho | 2023-01-13 16:44:25 +0100 |
---|---|---|
committer | Son HO | 2023-02-03 11:21:46 +0100 |
commit | c52add165764d3a0b68ee5181901109078e9b19b (patch) | |
tree | 782758a96e6b1a8b9998e631a2a91af193846459 /tests/coq/hashmap | |
parent | e69382acbcc4bdd27612c9cf8ec282db71f8408d (diff) |
Update the hashmap and regenerate
Diffstat (limited to 'tests/coq/hashmap')
-rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 0d55b171..f1af0c21 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -55,8 +55,8 @@ Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) := hash_map_new_with_capacity_fwd T n (32%usize) (4%usize) (5%usize) . -(** [hashmap::HashMap::{0}::clear_slots] *) -Fixpoint hash_map_clear_slots_loop_fwd_back +(** [hashmap::HashMap::{0}::clear] *) +Fixpoint hash_map_clear_loop_fwd_back (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) : result (vec (List_t T)) := @@ -68,21 +68,15 @@ Fixpoint hash_map_clear_slots_loop_fwd_back then ( i1 <- usize_add i 1%usize; slots0 <- vec_index_mut_back (List_t T) slots i ListNil; - hash_map_clear_slots_loop_fwd_back T n0 slots0 i1) + hash_map_clear_loop_fwd_back T n0 slots0 i1) else Return slots end . -(** [hashmap::HashMap::{0}::clear_slots] *) -Definition hash_map_clear_slots_fwd_back - (T : Type) (n : nat) (slots : vec (List_t T)) : result (vec (List_t T)) := - hash_map_clear_slots_loop_fwd_back T n slots (0%usize) -. - (** [hashmap::HashMap::{0}::clear] *) Definition hash_map_clear_fwd_back (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) := - v <- hash_map_clear_slots_fwd_back T n self.(Hash_map_slots); + v <- hash_map_clear_loop_fwd_back T n self.(Hash_map_slots) (0%usize); Return (mkHash_map_t (0%usize) self.(Hash_map_max_load_factor) self.(Hash_map_max_load) v) . |