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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Map1

Description

Non-empty maps.

Provides type `Map1` of non-empty maps.

Import: @

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

@

Synopsis

- unlessNullM :: Monad m => m (Map k a) -> (Map1 k a -> m ()) -> m ()
- ifNull :: Map k a -> b -> (Map1 k a -> b) -> b
- type Map1 = NEMap
- unlessNull :: Applicative m => Map k a -> (Map1 k a -> m ()) -> m ()
- module Data.Map.NonEmpty

# Documentation

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

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

type Map1 = NEMap Source #

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 ())`.

module Data.Map.NonEmpty