Function vstd::hash_set::axiom_hash_set_with_view_spec_len

source · 
pub broadcast proof fn axiom_hash_set_with_view_spec_len<Key>(m: &HashSetWithView<Key>)
where
    Key: View + Eq + Hash,
Expand description
ensures
#[trigger] m.spec_len() == m@.len(),