Function vstd::std_specs::hash::axiom_spec_hash_map_len

pub broadcast proof fn axiom_spec_hash_map_len<Key, Value, S>(m: &HashMap<Key, Value, S>)

Expand description

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> #[trigger] spec_hash_map_len(m) == m@.len(),

Function vstd::std_specs::hash::axiom_spec_hash_map_lenCopy item path