From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 19 Mar 2024 05:29:29 +0100 Subject: Regenerate the tests --- tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 6 ++---- 1 file changed, 2 insertions(+), 4 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 b16dcada..9b5baaeb 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -324,8 +324,7 @@ let hashmap_HashMap_get_mut_in_list (t : Type0) (ls : hashmap_List_t t) (key : usize) : result (t & (t -> result (hashmap_List_t t))) = - let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t ls key in - Return (x, back_'a) + hashmap_HashMap_get_mut_in_list_loop t ls key (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 *) @@ -446,8 +445,7 @@ let insert_on_disk (key : usize) (value : u64) (st : state) : result (state & unit) = let* (st1, hm) = hashmap_utils_deserialize st in let* hm1 = hashmap_HashMap_insert u64 hm key value in - let* (st2, _) = hashmap_utils_serialize hm1 st1 in - Return (st2, ()) + hashmap_utils_serialize hm1 st1 (** [hashmap_main::main]: Source: 'src/hashmap_main.rs', lines 16:0-16:13 *) -- cgit v1.2.3