vstd::hash_set

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