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/coq/hashmap_on_disk | |
| parent | ff9fe8aa1e13a7297f7c4f2c2554235361db038f (diff) | |
Regenerate the files
Diffstat (limited to 'tests/coq/hashmap_on_disk')
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index b74fa61a..6a7eeb2d 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -53,8 +53,9 @@ Definition hashmap_HashMap_new_with_capacity (max_load_divisor : usize) : result (hashmap_HashMap_t T) := - let v := alloc_vec_Vec_new (hashmap_List_t T) in - slots <- hashmap_HashMap_allocate_slots T n v capacity; + slots <- + hashmap_HashMap_allocate_slots T n (alloc_vec_Vec_new (hashmap_List_t T)) + capacity; i <- usize_mul capacity max_load_dividend; i1 <- usize_div i max_load_divisor; Return @@ -138,7 +139,7 @@ Fixpoint hashmap_HashMap_insert_in_list_loop let (b, back) := p in Return (b, Hashmap_List_Cons ckey cvalue back)) | Hashmap_List_Nil => - let l := Hashmap_List_Nil in Return (true, Hashmap_List_Cons key value l) + Return (true, Hashmap_List_Cons key value Hashmap_List_Nil) end end . @@ -424,8 +425,7 @@ Definition hashmap_HashMap_get_mut_in_list := p <- hashmap_HashMap_get_mut_in_list_loop T n ls key; let (t, back_'a) := p in - let back_'a1 := fun (ret : T) => back_'a ret in - Return (t, back_'a1) + Return (t, back_'a) . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: |