diff options
author | Son Ho | 2023-12-23 00:59:55 +0100 |
---|---|---|
committer | Son Ho | 2023-12-23 00:59:55 +0100 |
commit | a4decc7654bc6f3301c0174124d21fdbc2dbc708 (patch) | |
tree | f992f3bb64609bf12d033a1424873a8134c66617 /tests/fstar-split/hashmap | |
parent | ff9fe8aa1e13a7297f7c4f2c2554235361db038f (diff) |
Regenerate the files
Diffstat (limited to 'tests/fstar-split/hashmap')
-rw-r--r-- | tests/fstar-split/hashmap/Hashmap.Funs.fst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tests/fstar-split/hashmap/Hashmap.Funs.fst b/tests/fstar-split/hashmap/Hashmap.Funs.fst index 79327183..290d49ee 100644 --- a/tests/fstar-split/hashmap/Hashmap.Funs.fst +++ b/tests/fstar-split/hashmap/Hashmap.Funs.fst @@ -41,8 +41,8 @@ let hashMap_new_with_capacity (max_load_divisor : usize) : result (hashMap_t t) = - let v = alloc_vec_Vec_new (list_t t) in - let* slots = hashMap_allocate_slots t v capacity in + let* slots = hashMap_allocate_slots t (alloc_vec_Vec_new (list_t t)) capacity + in let* i = usize_mul capacity max_load_dividend in let* i1 = usize_div i max_load_divisor in Return @@ -124,7 +124,7 @@ let rec hashMap_insert_in_list_loop_back else let* tl1 = hashMap_insert_in_list_loop_back t key value tl in Return (List_Cons ckey cvalue tl1) - | List_Nil -> let l = List_Nil in Return (List_Cons key value l) + | List_Nil -> Return (List_Cons key value List_Nil) end (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: backward function 0 |