diff options
author | Son Ho | 2022-05-05 17:12:02 +0200 |
---|---|---|
committer | Son Ho | 2022-05-05 17:12:02 +0200 |
commit | bb94d52be2d0ddb317577dc3cd468754646e4b64 (patch) | |
tree | f7942a35620b09692ae34e68c7aa5e48485edef6 /tests/hashmap_on_disk/HashmapMain.Clauses.fst | |
parent | 643ffc01250e4ebdefe3a33e8b16ea9668db3356 (diff) |
Update the hashmap_on_disk example
Diffstat (limited to 'tests/hashmap_on_disk/HashmapMain.Clauses.fst')
-rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Clauses.fst | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.fst index 84e6494a..b864e32a 100644 --- a/tests/hashmap_on_disk/HashmapMain.Clauses.fst +++ b/tests/hashmap_on_disk/HashmapMain.Clauses.fst @@ -9,53 +9,53 @@ open HashmapMain.Types (** [hashmap::HashMap::allocate_slots]: decreases clause *) unfold let hashmap_hash_map_allocate_slots_decreases (t : Type0) (slots : vec (hashmap_list_t t)) - (n : usize) (st : state) : nat = n + (n : usize) : nat = n (** [hashmap::HashMap::clear_slots]: decreases clause *) unfold let hashmap_hash_map_clear_slots_decreases (t : Type0) (slots : vec (hashmap_list_t t)) - (i : usize) (st : state) : nat = + (i : usize) : nat = if i < length slots then length slots - i else 0 (** [hashmap::HashMap::insert_in_list]: decreases clause *) unfold let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t) - (ls : hashmap_list_t t) (st : state) : hashmap_list_t t = + (ls : hashmap_list_t t) : hashmap_list_t t = ls (** [hashmap::HashMap::move_elements_from_list]: decreases clause *) unfold let hashmap_hash_map_move_elements_from_list_decreases (t : Type0) - (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) (st : state) : hashmap_list_t t = + (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : hashmap_list_t t = ls (** [hashmap::HashMap::move_elements]: decreases clause *) unfold let hashmap_hash_map_move_elements_decreases (t : Type0) (ntable : hashmap_hash_map_t t) - (slots : vec (hashmap_list_t t)) (i : usize) (st : state) : nat = + (slots : vec (hashmap_list_t t)) (i : usize) : nat = if i < length slots then length slots - i else 0 (** [hashmap::HashMap::contains_key_in_list]: decreases clause *) unfold let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (key : usize) - (ls : hashmap_list_t t) (st : state) : hashmap_list_t t = + (ls : hashmap_list_t t) : hashmap_list_t t = ls (** [hashmap::HashMap::get_in_list]: decreases clause *) unfold -let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) (st : state) : +let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : hashmap_list_t t) : hashmap_list_t t = ls (** [hashmap::HashMap::get_mut_in_list]: decreases clause *) unfold let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize) - (ls : hashmap_list_t t) (st : state) : hashmap_list_t t = + (ls : hashmap_list_t t) : hashmap_list_t t = ls (** [hashmap::HashMap::remove_from_list]: decreases clause *) unfold let hashmap_hash_map_remove_from_list_decreases (t : Type0) (key : usize) - (ls : hashmap_list_t t) (st : state) : hashmap_list_t t = + (ls : hashmap_list_t t) : hashmap_list_t t = ls |