Function value_filter_choose Copy item path

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

{ choose |k: K| value_filter(m, f).contains_key(k) }