Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Null

Description

Overloaded null and empty for collections and sequences.

Synopsis

Documentation

class Null a where Source #

Minimal complete definition

empty

Methods

empty :: a Source #

null :: a -> Bool Source #

Satisfying null empty == True.

default null :: Eq a => a -> Bool Source #

Instances

Instances details
Null () Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: () Source #

null :: () -> Bool Source #

Null ByteString Source # 
Instance details

Defined in Agda.Utils.Null

Null IntSet Source # 
Instance details

Defined in Agda.Utils.Null

Null Doc Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: Doc Source #

null :: Doc -> Bool Source #

Null Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

Null ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Null Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Null Fixity Source # 
Instance details

Defined in Agda.Syntax.Common

Null FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Null QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Null Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Null Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Null Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Null PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null MutualInfo Source #

Default value for MutualInfo.

Instance details

Defined in Agda.Syntax.Info

Null LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null Clause Source #

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

Instance details

Defined in Agda.Syntax.Internal

Null MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Null Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null Fields Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null NLMState Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Null [a] Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: [a] Source #

null :: [a] -> Bool Source #

Null (Maybe a) Source #

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

Instance details

Defined in Agda.Utils.Null

Methods

empty :: Maybe a Source #

null :: Maybe a -> Bool Source #

Null (IntMap a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: IntMap a Source #

null :: IntMap a -> Bool Source #

Null (Seq a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: Seq a Source #

null :: Seq a -> Bool Source #

Null (Set a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: Set a Source #

null :: Set a -> Bool Source #

Null (Bag a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: Bag a Source #

null :: Bag a -> Bool Source #

Null (HashSet a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: HashSet a Source #

null :: HashSet a -> Bool Source #

Null (Maybe a) Source # 
Instance details

Defined in Agda.Utils.Maybe.Strict

Methods

empty :: Maybe a Source #

null :: Maybe a -> Bool Source #

Null a => Null (SizedThing a) Source # 
Instance details

Defined in Agda.Utils.Size

Null (Benchmark a) Source #

Initial benchmark structure (empty).

Instance details

Defined in Agda.Utils.Benchmark

Null (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

empty :: Range' a Source #

null :: Range' a -> Bool Source #

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null (WhereClause' a) Source #

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

Instance details

Defined in Agda.Syntax.Concrete

Null (Favorites a) Source # 
Instance details

Defined in Agda.Utils.Favorites

Null (CMSet cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

empty :: CMSet cinfo Source #

null :: CMSet cinfo -> Bool Source #

Null (CallGraph cinfo) Source #

null checks whether the call graph is completely disconnected.

Instance details

Defined in Agda.Termination.CallGraph

Methods

empty :: CallGraph cinfo Source #

null :: CallGraph cinfo -> Bool Source #

Null (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Null (Tele a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

empty :: Tele a Source #

null :: Tele a -> Bool Source #

Null (Case m) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

empty :: Case m Source #

null :: Case m -> Bool Source #

Null a => Null (MaybeWarnings' a) Source # 
Instance details

Defined in Agda.Interaction.Imports

Null (Match a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Match

Methods

empty :: Match a Source #

null :: Match a -> Bool Source #

(Null a, Null b) => Null (a, b) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: (a, b) Source #

null :: (a, b) -> Bool Source #

Null (Map k a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: Map k a Source #

null :: Map k a -> Bool Source #

Null (HashMap k a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: HashMap k a Source #

null :: HashMap k a -> Bool Source #

Null (Solution rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

empty :: Solution rigid flex Source #

null :: Solution rigid flex -> Bool Source #

Null (Trie k v) Source #

Empty trie.

Instance details

Defined in Agda.Utils.Trie

Methods

empty :: Trie k v Source #

null :: Trie k v -> Bool Source #

Null (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Using' n m Source #

null :: Using' n m -> Bool Source #

Null (ImportDirective' n m) Source #

null for import directives holds when everything is imported unchanged (no names are hidden or renamed).

Instance details

Defined in Agda.Syntax.Common

Monad m => Null (PureConversionT m Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

(Null (m a), Monad m) => Null (ReaderT r m a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: ReaderT r m a Source #

null :: ReaderT r m a -> Bool Source #

(Null (m a), Monad m) => Null (StateT r m a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: StateT r m a Source #

null :: StateT r m a -> Bool Source #

Testing for null.

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

ifNotNull :: Null a => a -> (a -> b) -> b -> b Source #

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

ifNotNullM :: (Monad m, Null a) => m a -> (a -> m b) -> m b -> m b Source #

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

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

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

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