Function vstd::hash_map::axiom_hash_map_with_view_spec_len

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