diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 8 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 10 |
2 files changed, 8 insertions, 10 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 5cd9fe70..0478edbe 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -49,8 +49,7 @@ Definition hashMap_new_with_capacity (max_load_divisor : usize) : result (HashMap_t T) := - let v := alloc_vec_Vec_new (List_t T) in - slots <- hashMap_allocate_slots T n v capacity; + slots <- hashMap_allocate_slots T n (alloc_vec_Vec_new (List_t T)) capacity; i <- usize_mul capacity max_load_dividend; i1 <- usize_div i max_load_divisor; Return @@ -128,7 +127,7 @@ Fixpoint hashMap_insert_in_list_loop p <- hashMap_insert_in_list_loop T n1 key value tl; let (b, back) := p in Return (b, List_Cons ckey cvalue back)) - | List_Nil => let l := List_Nil in Return (true, List_Cons key value l) + | List_Nil => Return (true, List_Cons key value List_Nil) end end . @@ -401,8 +400,7 @@ Definition hashMap_get_mut_in_list := p <- 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::{hashmap::HashMap<T>}::get_mut]: 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]: |