Skip to main content

project_first_key

Function project_first_key 

Source
pub open spec fn project_first_key<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1) -> Map<K2, V>
Expand description
{
    Map::new(
        m.dom().filter(|p: (K1, K2)| p.0 == k1).map(|p: (K1, K2)| p.1),
        |k2: K2| m[(k1, k2)],
    )
}

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