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/fstar/hashmap | |
| parent | 5a1373f5492f65ff0da6f7e0c34b056a98070908 (diff) | |
Regenerate the tests
Diffstat (limited to 'tests/fstar/hashmap')
| -rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 447f9b49..7ca8b9c1 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -308,8 +308,7 @@ let hashMap_get_mut_in_list (t : Type0) (ls : list_t t) (key : usize) : result (t & (t -> result (list_t t))) = - let* (x, back_'a) = hashMap_get_mut_in_list_loop t ls key in - Return (x, back_'a) + hashMap_get_mut_in_list_loop t ls key (** [hashmap::{hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 *) |