Function vstd::std_specs::hash::ex_hash_set_remove

source · 
pub exec fn ex_hash_set_remove<Key, S, Q>(m: &mut HashSet<Key, S>, k: &Q) -> result : bool
where
    Key: Borrow<Q> + Hash + Eq,
    Q: Hash + Eq + ?Sized,
    S: BuildHasher,
Expand description
ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& sets_differ_by_borrowed_key(old(m)@, m@, k)
        &&& result == set_contains_borrowed_key(old(m)@, k)

    },