From 975ddb208f18cb4ba46293dd788c46eb1ce43938 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 11:58:44 +0200 Subject: Regenerate the test files --- tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) (limited to 'tests/fstar/hashmap_on_disk') diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index 97f4151f..09928620 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -305,15 +305,14 @@ let rec hashmap_HashMap_get_mut_in_list_loop | Hashmap_List_Cons ckey cvalue tl -> if ckey = key then - let back_'a = fun ret -> Return (Hashmap_List_Cons ckey ret tl) in - Return (cvalue, back_'a) + let back = fun ret -> Return (Hashmap_List_Cons ckey ret tl) in + Return (cvalue, back) else - let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t tl key in - let back_'a1 = + let* (x, back) = hashmap_HashMap_get_mut_in_list_loop t tl key in + let back1 = fun ret -> - let* tl1 = back_'a ret in Return (Hashmap_List_Cons ckey cvalue tl1) - in - Return (x, back_'a1) + let* tl1 = back ret in Return (Hashmap_List_Cons ckey cvalue tl1) in + Return (x, back1) | Hashmap_List_Nil -> Fail Failure end @@ -339,12 +338,12 @@ let hashmap_HashMap_get_mut (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) self.slots hash_mod in let* (x, get_mut_in_list_back) = hashmap_HashMap_get_mut_in_list t l key in - let back_'a = + let back = fun ret -> let* l1 = get_mut_in_list_back ret in let* v = index_mut_back l1 in Return { self with slots = v } in - Return (x, back_'a) + Return (x, back) (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: loop 0: Source: 'src/hashmap.rs', lines 265:4-291:5 *) -- cgit v1.2.3