vstd::hash_map

Function 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(),