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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Set1

Description

Non-empty sets.

Provides type `Set1` of non-empty sets.

Import: @

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

@

Synopsis

- unlessNullM :: Monad m => m (Set a) -> (Set1 a -> m ()) -> m ()
- type Set1 = NESet
- ifNull :: Set a -> b -> (Set1 a -> b) -> b
- unlessNull :: Applicative m => Set a -> (Set1 a -> m ()) -> m ()
- toSet' :: Maybe (Set1 a) -> Set a
- module Data.Set.NonEmpty

# Documentation

unlessNullM :: Monad m => m (Set a) -> (Set1 a -> m ()) -> m () Source #

type Set1 = NESet Source #

ifNull :: Set a -> b -> (Set1 a -> b) -> b Source #

unlessNull :: Applicative m => Set a -> (Set1 a -> m ()) -> m () Source #

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

toSet' :: Maybe (Set1 a) -> Set a Source #

Lossless `toSet`. Opposite of `nonEmptySet`.

module Data.Set.NonEmpty