Function vstd::hash_set::axiom_string_hash_set_spec_len

source · 
pub broadcast proof fn axiom_string_hash_set_spec_len(m: &StringHashSet)
Expand description
ensures
#[trigger] m.spec_len() == m@.len(),