Function vstd::hash_map::axiom_string_hash_map_spec_len

source · 
pub broadcast proof fn axiom_string_hash_map_spec_len<Value>(m: &StringHashMap<Value>)
Expand description
ensures
#[trigger] m.spec_len() == m@.len(),