Function vstd::std_specs::hash::ex_hash_set_insert

source · 
pub exec fn ex_hash_set_insert<Key, S>(m: &mut HashSet<Key, S>, k: Key) -> result : bool
where
    Key: Eq + Hash,
    S: BuildHasher,
Expand description
ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& m@ == old(m)@.insert(k)
        &&& result == !old(m)@.contains(k)

    },