Agda
Safe HaskellNone
LanguageHaskell2010

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

Documentation

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

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

Lossless toSet. Opposite of nonEmptySet.

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

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