project_second_key

Function project_second_key 

Source
pub open spec fn project_second_key<K1, K2, V>(m: Map<(K1, K2), V>, k2: K2) -> Map<K1, V>
Expand description
{ Map::new(|k1: K1| m.contains_key((k1, k2)), |k1: K1| m[(k1, k2)]) }

Returns a new map that projects the second key of a pair (K1, K2), keeping the values associated with the first key K1.