Function axiom_spec_hash_map_iter

Help

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

Expand description

ensures

({
    let (pos, v) = #[trigger] spec_hash_map_iter(m)@;
    &&& pos == 0int
    &&& forall |i: int| 0 <= i < v.len() ==> #[trigger] m@[v[i].0] == v[i].1

}),

Function axiom_spec_hash_map_iterCopy item path

Function axiom_spec_hash_map_iter