Agda.Utils.Null

Overloaded null and empty for collections and sequences.

Documentation

class Null a where

Minimal complete definition

empty

Methods

empty :: a

null :: a -> Bool

Satisfying null empty == True.

Instances

Null ()

Null ByteString

Null IntSet

Null Permutation

Null ClauseBody

Null Clause

A null clause is one with no patterns and no rhs. Should not exist in practice.

Null Simplification

Null Fields

Null ProblemRest

Null [a]

Null (Maybe a)

A Maybe is null when it corresponds to the empty list.

Null (IntMap a)

Null (Set a)

Null (Seq a)

Null (Bag a)

Null a => Null (SizedThing a)

Null (Favorites a)

Null (CMSet cinfo)

Null (CallGraph cinfo)

null checks whether the call graph is completely disconnected.

Null (Range' a)

Null (Tele a)

Null (Match a)

Null a => Null (Problem' a)

(Null a, Null b) => Null (a, b)

Null (Map k a)

Testing for null.

ifNull :: Null a => a -> b -> (a -> b) -> b

ifNullM :: (Monad m, Null a) => m a -> m b -> (a -> m b) -> m b

whenNull :: (Monad m, Null a) => a -> m () -> m ()

unlessNull :: (Monad m, Null a) => a -> (a -> m ()) -> m ()

whenNullM :: (Monad m, Null a) => m a -> m () -> m ()

unlessNullM :: (Monad m, Null a) => m a -> (a -> m ()) -> m ()