diff options
| author | Son Ho | 2024-03-19 05:29:29 +0100 |
|---|---|---|
| committer | Son Ho | 2024-03-19 05:29:29 +0100 |
| commit | f3e16bb43a8ff27a5184d9fa452277cc6a59410f (patch) | |
| tree | f79760b40b3a9f404b1db0d61f9d452408ef1de5 /tests/coq/hashmap/Hashmap_Funs.v | |
| parent | 5a1373f5492f65ff0da6f7e0c34b056a98070908 (diff) | |
Regenerate the tests
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 0478edbe..ab424e42 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -398,9 +398,7 @@ Definition hashMap_get_mut_in_list (T : Type) (n : nat) (ls : List_t T) (key : usize) : result (T * (T -> result (List_t T))) := - p <- hashMap_get_mut_in_list_loop T n ls key; - let (t, back_'a) := p in - Return (t, back_'a) + hashMap_get_mut_in_list_loop T n ls key . (** [hashmap::{hashmap::HashMap<T>}::get_mut]: |