Function vstd::std_specs::hash::ex_hash_set_get

source ·

pub exec fn ex_hash_set_get<'a, Key, S, Q>(
    m: &'a HashSet<Key, S>,
    k: &Q
) -> result : Option<&'a Key>where
    Key: Borrow<Q> + Hash + Eq,
    Q: Hash + Eq + ?Sized,
    S: BuildHasher,

Expand description

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> match result {
        Some(v) => sets_borrowed_key_to_key(m@, k, v),
        None => !set_contains_borrowed_key(m@, k),
    },