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.

null :: Eq a => a -> Bool

Satisfying null empty == True.

Instances

Null ()

Methods

empty :: ()

null :: () -> Bool

Null ByteString

Methods

empty :: ByteString

null :: ByteString -> Bool

Null IntSet

Methods

empty :: IntSet

null :: IntSet -> Bool

Null Doc

Methods

empty :: Doc

null :: Doc -> Bool

Null Occurrence

Methods

empty :: Occurrence

null :: Occurrence -> Bool

Null Permutation

Methods

empty :: Permutation

null :: Permutation -> Bool

Null PatInfo

Methods

empty :: PatInfo

null :: PatInfo -> Bool

Null LHSInfo

Methods

empty :: LHSInfo

null :: LHSInfo -> Bool

Null LetInfo

Methods

empty :: LetInfo

null :: LetInfo -> Bool

Null ExprInfo

Methods

empty :: ExprInfo

null :: ExprInfo -> Bool

Null ClauseBody

Methods

empty :: ClauseBody

null :: ClauseBody -> Bool

Null Clause

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

Methods

empty :: Clause

null :: Clause -> Bool

Null FreeVars

Methods

empty :: FreeVars

null :: FreeVars -> Bool

Null Simplification

Methods

empty :: Simplification

null :: Simplification -> Bool

Null Fields

Methods

empty :: Fields

null :: Fields -> Bool

Null ProblemRest

Methods

empty :: ProblemRest

null :: ProblemRest -> Bool

Null Edge

Methods

empty :: Edge

null :: Edge -> Bool

Null [a]

Methods

empty :: [a]

null :: [a] -> Bool

Null (Maybe a)

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

Methods

empty :: Maybe a

null :: Maybe a -> Bool

Null (IntMap a)

Methods

empty :: IntMap a

null :: IntMap a -> Bool

Null (Seq a)

Methods

empty :: Seq a

null :: Seq a -> Bool

Null (Set a)

Methods

empty :: Set a

null :: Set a -> Bool

Null (HashSet a)

Methods

empty :: HashSet a

null :: HashSet a -> Bool

Null (Bag a)

Methods

empty :: Bag a

null :: Bag a -> Bool

Null (Favorites a)

Methods

empty :: Favorites a

null :: Favorites a -> Bool

Null a => Null (SizedThing a)

Methods

empty :: SizedThing a

null :: SizedThing a -> Bool

Null (Benchmark a)

Initial benchmark structure (empty).

Methods

empty :: Benchmark a

null :: Benchmark a -> Bool

Null (CMSet cinfo)

Methods

empty :: CMSet cinfo

null :: CMSet cinfo -> Bool

Null (CallGraph cinfo)

null checks whether the call graph is completely disconnected.

Methods

empty :: CallGraph cinfo

null :: CallGraph cinfo -> Bool

Null (Range' a)

Methods

empty :: Range' a

null :: Range' a -> Bool

Null (TCM Doc)

Methods

empty :: TCM Doc

null :: TCM Doc -> Bool

Null (WhereClause' a)

A WhereClause is null when the where keyword is absent. An empty list of declarations does not count as null here.

Methods

empty :: WhereClause' a

null :: WhereClause' a -> Bool

Null (Tele a)

Methods

empty :: Tele a

null :: Tele a -> Bool

Null (Case m)

Methods

empty :: Case m

null :: Case m -> Bool

Null (Match a)

Methods

empty :: Match a

null :: Match a -> Bool

Null a => Null (Problem' a)

Methods

empty :: Problem' a

null :: Problem' a -> Bool

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

Methods

empty :: (a, b)

null :: (a, b) -> Bool

Null (Map k a)

Methods

empty :: Map k a

null :: Map k a -> Bool

Null (HashMap k a)

Methods

empty :: HashMap k a

null :: HashMap k a -> Bool

Null (Trie k v)

Empty trie.

Methods

empty :: Trie k v

null :: Trie k v -> Bool

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