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.

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

Instances

Null ()

Defined in Agda.Utils.Null

Methods

empty :: ()

null :: () -> Bool

Null ByteString

Defined in Agda.Utils.Null

Methods

empty :: ByteString

null :: ByteString -> Bool

Null ByteString

Defined in Agda.Utils.Null

Methods

empty :: ByteString

null :: ByteString -> Bool

Null Text

Defined in Agda.Utils.Null

Methods

empty :: Text

null :: Text -> Bool

Null IntSet

Defined in Agda.Utils.Null

Methods

empty :: IntSet

null :: IntSet -> Bool

Null Doc

Defined in Agda.Utils.Null

Methods

empty :: Doc

null :: Doc -> Bool

Null Permutation

Defined in Agda.Utils.Permutation

Methods

empty :: Permutation

null :: Permutation -> Bool

Null ExpandedEllipsis

Defined in Agda.Syntax.Common

Methods

empty :: ExpandedEllipsis

null :: ExpandedEllipsis -> Bool

Null Fixity'

Defined in Agda.Syntax.Common

Methods

empty :: Fixity'

null :: Fixity' -> Bool

Null Fixity

Defined in Agda.Syntax.Common

Methods

empty :: Fixity

null :: Fixity -> Bool

Null FixityLevel

Defined in Agda.Syntax.Common

Methods

empty :: FixityLevel

null :: FixityLevel -> Bool

Null QωOrigin

Defined in Agda.Syntax.Common

Methods

empty :: QωOrigin

null :: QωOrigin -> Bool

Null Q1Origin

Defined in Agda.Syntax.Common

Methods

empty :: Q1Origin

null :: Q1Origin -> Bool

Null Q0Origin

Defined in Agda.Syntax.Common

Methods

empty :: Q0Origin

null :: Q0Origin -> Bool

Null Range

Defined in Agda.Interaction.Highlighting.Range

Methods

empty :: Range

null :: Range -> Bool

Null Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

empty :: Occurrence

null :: Occurrence -> Bool

Null ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

empty :: ScopeInfo

null :: ScopeInfo -> Bool

Null Scope

Defined in Agda.Syntax.Scope.Base

Methods

empty :: Scope

null :: Scope -> Bool

Null PatInfo

Defined in Agda.Syntax.Info

Methods

empty :: PatInfo

null :: PatInfo -> Bool

Null LHSInfo

Defined in Agda.Syntax.Info

Methods

empty :: LHSInfo

null :: LHSInfo -> Bool

Null MutualInfo

Default value for MutualInfo.

Defined in Agda.Syntax.Info

Methods

empty :: MutualInfo

null :: MutualInfo -> Bool

Null LetInfo

Defined in Agda.Syntax.Info

Methods

empty :: LetInfo

null :: LetInfo -> Bool

Null ExprInfo

Defined in Agda.Syntax.Info

Methods

empty :: ExprInfo

null :: ExprInfo -> Bool

Null Clause

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

Defined in Agda.Syntax.Internal

Methods

empty :: Clause

null :: Clause -> Bool

Null MetaSet

Defined in Agda.TypeChecking.Free.Lazy

Methods

empty :: MetaSet

null :: MetaSet -> Bool

Null WhereDeclarations

Defined in Agda.Syntax.Abstract

Methods

empty :: WhereDeclarations

null :: WhereDeclarations -> Bool

Null Simplification

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: Simplification

null :: Simplification -> Bool

Null Fields

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: Fields

null :: Fields -> Bool

Null ProjLams

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: ProjLams

null :: ProjLams -> Bool

Null MutualBlock

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: MutualBlock

null :: MutualBlock -> Bool

Null LeftoverPatterns

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

empty :: LeftoverPatterns

null :: LeftoverPatterns -> Bool

Null NLMState

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

empty :: NLMState

null :: NLMState -> Bool

Null [a]

Defined in Agda.Utils.Null

Methods

empty :: [a]

null :: [a] -> Bool

Null (Maybe a)

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

Defined in Agda.Utils.Null

Methods

empty :: Maybe a

null :: Maybe a -> Bool

Null (IntMap a)

Defined in Agda.Utils.Null

Methods

empty :: IntMap a

null :: IntMap a -> Bool

Null (Seq a)

Defined in Agda.Utils.Null

Methods

empty :: Seq a

null :: Seq a -> Bool

Null (Set a)

Defined in Agda.Utils.Null

Methods

empty :: Set a

null :: Set a -> Bool

Null (Maybe a)

Defined in Agda.Utils.Maybe.Strict

Methods

empty :: Maybe a

null :: Maybe a -> Bool

Null (HashSet a)

Defined in Agda.Utils.Null

Methods

empty :: HashSet a

null :: HashSet a -> Bool

Null (Bag a)

Defined in Agda.Utils.Null

Methods

empty :: Bag a

null :: Bag a -> Bool

Null a => Null (SizedThing a)

Defined in Agda.Utils.Size

Methods

empty :: SizedThing a

null :: SizedThing a -> Bool

Null (Benchmark a)

Initial benchmark structure (empty).

Defined in Agda.Utils.Benchmark

Methods

empty :: Benchmark a

null :: Benchmark a -> Bool

Null (Range' a)

Defined in Agda.Syntax.Position

Methods

empty :: Range' a

null :: Range' a -> Bool

Null (TCM Doc)

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCM Doc

null :: TCM Doc -> Bool

Null (RangeMap a)

Defined in Agda.Utils.RangeMap

Methods

empty :: RangeMap a

null :: RangeMap a -> 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.

Defined in Agda.Syntax.Concrete

Methods

empty :: WhereClause' a

null :: WhereClause' a -> Bool

Null (Favorites a)

Defined in Agda.Utils.Favorites

Methods

empty :: Favorites a

null :: Favorites a -> Bool

Null (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

empty :: CMSet cinfo

null :: CMSet cinfo -> Bool

Null (CallGraph cinfo)

null checks whether the call graph is completely disconnected.

Defined in Agda.Termination.CallGraph

Methods

empty :: CallGraph cinfo

null :: CallGraph cinfo -> Bool

Null (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

empty :: Substitution' a

null :: Substitution' a -> Bool

Null (Tele a)

Defined in Agda.Syntax.Internal

Methods

empty :: Tele a

null :: Tele a -> Bool

Null (Case m)

Defined in Agda.TypeChecking.CompiledClause

Methods

empty :: Case m

null :: Case m -> Bool

Null (Match a)

Defined in Agda.TypeChecking.Patterns.Match

Methods

empty :: Match a

null :: Match a -> Bool

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

Defined in Agda.Utils.Null

Methods

empty :: (a, b)

null :: (a, b) -> Bool

Null (Map k a)

Defined in Agda.Utils.Null

Methods

empty :: Map k a

null :: Map k a -> Bool

Null (HashMap k a)

Defined in Agda.Utils.Null

Methods

empty :: HashMap k a

null :: HashMap k a -> Bool

Null (Trie k v)

Empty trie.

Defined in Agda.Utils.Trie

Methods

empty :: Trie k v

null :: Trie k v -> Bool

Null (Solution rigid flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

empty :: Solution rigid flex

null :: Solution rigid flex -> Bool

Null (BiMap k v)

Defined in Agda.Utils.BiMap

Methods

empty :: BiMap k v

null :: BiMap k v -> Bool

Null (Using' n m)

Defined in Agda.Syntax.Common

Methods

empty :: Using' n m

null :: Using' n m -> Bool

Null (ImportDirective' n m)

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

Defined in Agda.Syntax.Common

Methods

empty :: ImportDirective' n m

null :: ImportDirective' n m -> Bool

(MonadIO m, Null a) => Null (TCMT m a)

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCMT m a

null :: TCMT m a -> Bool

Monad m => Null (PureConversionT m Doc)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

empty :: PureConversionT m Doc

null :: PureConversionT m Doc -> Bool

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

Defined in Agda.Utils.Null

Methods

empty :: (a, b, c)

null :: (a, b, c) -> Bool

(Null (m a), Monad m) => Null (ReaderT r m a)

Defined in Agda.Utils.Null

Methods

empty :: ReaderT r m a

null :: ReaderT r m a -> Bool

(Null (m a), Monad m) => Null (StateT r m a)

Defined in Agda.Utils.Null

Methods

empty :: StateT r m a

null :: StateT r m a -> Bool

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

Defined in Agda.Utils.Null

Methods

empty :: (a, b, c, d)

null :: (a, b, c, d) -> Bool

Testing for null.

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

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

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

ifNotNullM :: (Monad m, Null a) => m a -> (a -> m b) -> 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 ()