Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Map1

Description

Non-empty maps.

Provides type Map1 of non-empty maps.

Import: @

import Agda.Utils.Map1 (Map1) import Agda.Utils.Map1 qualified as Map1

@

Synopsis

Documentation

ifNull :: Map k a -> b -> (Map1 k a -> b) -> b Source #

mapKeysAndValuesMonotonic :: (k -> k) -> (a -> b) -> Map1 k a -> Map1 k b Source #

Map both keys and values where the map is monotonic for the keys.

A function that maps both keys and values while preserving the map structure is missing in Data.Map.NonEmpty. We implement it simplistically here as a combination of mapKeysMonotonic and fmap.

unlessNull :: Applicative m => Map k a -> (Map1 k a -> m ()) -> m () Source #

A more general type would be Null m => Map k a -> (Map1 k a -> m) -> m but this type is problematic as we do not have a general instance Applicative m => Null (m ()).

unlessNullM :: Monad m => m (Map k a) -> (Map1 k a -> m ()) -> m () Source #