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

Safe HaskellNone
LanguageHaskell98

Agda.Utils.Null

Contents

Description

Overloaded null and empty for collections and sequences.

Synopsis

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