diff options
author | Son Ho | 2024-04-04 13:21:47 +0200 |
---|---|---|
committer | Son Ho | 2024-04-04 13:21:47 +0200 |
commit | 46f64c1b9f3bfc2703186b32a74c611e0e43f63f (patch) | |
tree | 77ef3b93f65698cbe907b93d2db0bb5f23227c1b /tests/fstar/hashmap | |
parent | bac38f94aacf4a0d621b0b2d2c423db9e0c6f175 (diff) |
Regenerate the test files
Diffstat (limited to 'tests/fstar/hashmap')
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst index 0e770ac9..d897933a 100644 --- a/tests/fstar/hashmap/Hashmap.Funs.fst +++ b/tests/fstar/hashmap/Hashmap.Funs.fst @@ -79,8 +79,8 @@ let rec hashMap_clear_loop (** [hashmap::{hashmap::HashMap<T>}::clear]: Source: 'src/hashmap.rs', lines 80:4-80:27 *) let hashMap_clear (t : Type0) (self : hashMap_t t) : result (hashMap_t t) = - let* back = hashMap_clear_loop t self.slots 0 in - Return { self with num_entries = 0; slots = back } + let* hm = hashMap_clear_loop t self.slots 0 in + Return { self with num_entries = 0; slots = hm } (** [hashmap::{hashmap::HashMap<T>}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 *) @@ -99,8 +99,8 @@ let rec hashMap_insert_in_list_loop if ckey = key then Return (false, List_Cons ckey value tl) else - let* (b, back) = hashMap_insert_in_list_loop t key value tl in - Return (b, List_Cons ckey cvalue back) + let* (b, tl1) = hashMap_insert_in_list_loop t key value tl in + Return (b, List_Cons ckey cvalue tl1) | List_Nil -> Return (true, List_Cons key value List_Nil) end @@ -344,8 +344,8 @@ let rec hashMap_remove_from_list_loop | List_Nil -> Fail Failure end else - let* (o, back) = hashMap_remove_from_list_loop t key tl in - Return (o, List_Cons ckey x back) + let* (o, tl1) = hashMap_remove_from_list_loop t key tl in + Return (o, List_Cons ckey x tl1) | List_Nil -> Return (None, List_Nil) end |