Function forall_map_values Copy item path

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

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