Skip to content

Commit 62362b0

Browse files
authored
Small changes to hash decreases axioms (#1816)
1 parent 35ad1ca commit 62362b0

1 file changed

Lines changed: 4 additions & 4 deletions

File tree

source/vstd/std_specs/hash.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1059,7 +1059,7 @@ pub assume_specification<'a, Key, Value, S>[ HashMap::<Key, Value, S>::values ](
10591059
},
10601060
;
10611061

1062-
pub broadcast proof fn axiom_hashmap_index_decreases<Key, Value>(m: HashMap<Key, Value>)
1062+
pub broadcast proof fn axiom_hashmap_decreases<Key, Value, S>(m: HashMap<Key, Value, S>)
10631063
ensures
10641064
#[trigger] (decreases_to!(m => m@)),
10651065
{
@@ -1397,7 +1397,7 @@ pub assume_specification<'a, Key, S>[ HashSet::<Key, S>::iter ](m: &'a HashSet<K
13971397
},
13981398
;
13991399

1400-
pub broadcast proof fn axiom_hashset_index_decreases<Key>(m: HashSet<Key>)
1400+
pub broadcast proof fn axiom_hashset_decreases<Key, S>(m: HashSet<Key, S>)
14011401
ensures
14021402
#[trigger] (decreases_to!(m => m@)),
14031403
{
@@ -1438,8 +1438,8 @@ pub broadcast group group_hash_axioms {
14381438
axiom_set_box_key_to_value,
14391439
axiom_spec_hash_set_len,
14401440
axiom_spec_hash_map_iter,
1441-
axiom_hashmap_index_decreases,
1442-
axiom_hashset_index_decreases,
1441+
axiom_hashmap_decreases,
1442+
axiom_hashset_decreases,
14431443
}
14441444

14451445
} // verus!

0 commit comments

Comments
 (0)