diff options
Diffstat (limited to 'tests/fstar/hashmap_on_disk')
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 09928620..e0005c81 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -84,8 +84,8 @@ let rec hashmap_HashMap_clear_loop Source: 'src/hashmap.rs', lines 80:4-80:27 *) let hashmap_HashMap_clear (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) = - let* back = hashmap_HashMap_clear_loop t self.slots 0 in - Return { self with num_entries = 0; slots = back } + let* hm = hashmap_HashMap_clear_loop t self.slots 0 in + Return { self with num_entries = 0; slots = hm } (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 *) @@ -105,8 +105,8 @@ let rec hashmap_HashMap_insert_in_list_loop if ckey = key then Return (false, Hashmap_List_Cons ckey value tl) else - let* (b, back) = hashmap_HashMap_insert_in_list_loop t key value tl in - Return (b, Hashmap_List_Cons ckey cvalue back) + let* (b, tl1) = hashmap_HashMap_insert_in_list_loop t key value tl in + Return (b, Hashmap_List_Cons ckey cvalue tl1) | Hashmap_List_Nil -> Return (true, Hashmap_List_Cons key value Hashmap_List_Nil) end @@ -364,8 +364,8 @@ let rec hashmap_HashMap_remove_from_list_loop | Hashmap_List_Nil -> Fail Failure end else - let* (o, back) = hashmap_HashMap_remove_from_list_loop t key tl in - Return (o, Hashmap_List_Cons ckey x back) + let* (o, tl1) = hashmap_HashMap_remove_from_list_loop t key tl in + Return (o, Hashmap_List_Cons ckey x tl1) | Hashmap_List_Nil -> Return (None, Hashmap_List_Nil) end |