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 Doc

Null PatInfo

Null LHSInfo

Null LetInfo

Null ExprInfo

Null Occurrence

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 Edge

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 (HashSet a)

Null (Bag a)

Null a => Null (SizedThing a)

Null (Favorites a)

Null (Benchmark a)

Initial benchmark structure (empty).

Null (CMSet cinfo)

Null (CallGraph cinfo)

null checks whether the call graph is completely disconnected.

Null (Range' a)

Null (TCM Doc)

Null (Tele a)

Null (Case m)

Null (Match a)

Null a => Null (Problem' a)

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

Null (Map k a)

Null (HashMap k a)

Null (Trie k v)

Empty trie.

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