Function forall_map Copy item path

pub open spec fn forall_map<K, V>(map: Map<K, V>, f: FnSpec<(K, V), bool>) -> bool

{ forall |k| #[trigger] map.contains_key(k) ==> f(k, map[k]) }