Function vstd::std_specs::hash::axiom_spec_hash_set_len

source · 
pub broadcast proof fn axiom_spec_hash_set_len<Key, S>(m: &HashSet<Key, S>)
Expand description
ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> #[trigger] spec_hash_set_len(m) == m@.len(),