Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Map

Contents

Synopsis
  • data EitherOrBoth a b
    • = L a
    • | B a b
    • | R b
  • unionWithM :: (Ord k, Monad m) => (a -> a -> m a) -> Map k a -> Map k a -> m (Map k a)
  • insertWithKeyM :: (Ord k, Monad m) => (k -> a -> a -> m a) -> k -> a -> Map k a -> m (Map k a)
  • allWithKey :: (k -> a -> Bool) -> Map k a -> Bool
  • filterKeys :: (k -> Bool) -> Map k a -> Map k a
  • unzip :: Map k (a, b) -> (Map k a, Map k b)
  • unzip3 :: Map k (a, b, c) -> (Map k a, Map k b, Map k c)

Monadic map operations

data EitherOrBoth a b Source #

Constructors

L a 
B a b 
R b 

unionWithM :: (Ord k, Monad m) => (a -> a -> m a) -> Map k a -> Map k a -> m (Map k a) Source #

Not very efficient (goes via a list), but it'll do.

insertWithKeyM :: (Ord k, Monad m) => (k -> a -> a -> m a) -> k -> a -> Map k a -> m (Map k a) Source #

Non-monadic map operations

allWithKey :: (k -> a -> Bool) -> Map k a -> Bool Source #

Big conjunction over a map.

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

Filter a map based on the keys.

unzip :: Map k (a, b) -> (Map k a, Map k b) Source #

Unzip a map.

unzip3 :: Map k (a, b, c) -> (Map k a, Map k b, Map k c) Source #