Agda.Utils.Map

Monadic map operations

adjustM :: (Functor f, Ord k) => (v -> f v) -> k -> Map k v -> f (Map k v)

Update monadically the value at one position (must exist!).

adjustM' :: (Functor f, Ord k) => (v -> f (a, v)) -> k -> Map k v -> f (a, Map k v)

Wrapper for adjustM for convenience.

Non-monadic map operations

filterKeys :: (k -> Bool) -> Map k a -> Map k a

Filter a map based on the keys.

mapMaybeKeys :: (Ord k1, Ord k2) => (k1 -> Maybe k2) -> Map k1 a -> Map k2 a

O(n log n). Rebuilds the map from scratch. Not worse than mapKeys.