Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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 Range Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Range

Null WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Abstract

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 Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Null Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Null QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Null ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null MutualInfo Source #

Default value for MutualInfo.

Instance details

Defined in Agda.Syntax.Info

Null PatInfo 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 Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Null ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Null MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Null Fields Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Null NLMState Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Null LeftoverPatterns Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Null Permutation Source # 
Instance details

Defined in Agda.Utils.Permutation

Null ProfileOptions Source # 
Instance details

Defined in Agda.Utils.ProfileOptions

Null ByteString Source # 
Instance details

Defined in Agda.Utils.Null

Null ByteString Source # 
Instance details

Defined in Agda.Utils.Null

Null IntSet Source # 
Instance details

Defined in Agda.Utils.Null

Null Text Source # 
Instance details

Defined in Agda.Utils.Null

Null () Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: () Source #

null :: () -> Bool Source #

Null Bool Source #

Viewing Bool as Maybe (), a boolean is null when it is false.

Instance details

Defined in Agda.Utils.Null

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 a => Null (Nice a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Monad

Methods

empty :: Nice a Source #

null :: Nice a -> 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 (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

empty :: Range' a Source #

null :: Range' a -> Bool Source #

Null (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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 (CMSet cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

empty :: CMSet cinfo Source #

null :: CMSet cinfo -> Bool Source #

Null (Case m) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

empty :: Case m Source #

null :: Case m -> Bool Source #

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null (Match a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Match

Methods

empty :: Match a Source #

null :: Match 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 (Benchmark a) Source #

Initial benchmark structure (empty).

Instance details

Defined in Agda.Utils.Benchmark

Null (Favorites a) Source # 
Instance details

Defined in Agda.Utils.Favorites

Null (RangeMap a) Source # 
Instance details

Defined in Agda.Utils.RangeMap

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

Defined in Agda.Utils.Size

SmallSetElement a => Null (SmallSet a) Source # 
Instance details

Defined in Agda.Utils.SmallSet

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

Defined in Agda.Utils.Null

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 a => Null (IO a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: IO a Source #

null :: IO 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 (Doc a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: Doc a Source #

null :: Doc 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 (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 [a] Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: [a] Source #

null :: [a] -> 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

Null (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Using' n m Source #

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

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

Defined in Agda.TypeChecking.Conversion.Pure

(MonadIO m, Null a) => Null (TCMT m a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCMT m a Source #

null :: TCMT m 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 (BiMap k v) Source # 
Instance details

Defined in Agda.Utils.BiMap

Methods

empty :: BiMap k v Source #

null :: BiMap k v -> 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 (WithDefault' a b) Source #

The null value of 'WithDefault b' is Default.

Instance details

Defined in Agda.Utils.WithDefault

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 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 (m a), Monad m) => Null (ExceptT e m a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: ExceptT e m a Source #

null :: ExceptT e m a -> Bool Source #

(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 s m a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: StateT s m a Source #

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

(Null (m a), Monad m, Monoid w) => Null (WriterT w m a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: WriterT w m a Source #

null :: WriterT w m a -> Bool Source #

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

Defined in Agda.Utils.Null

Methods

empty :: (a, b, c) Source #

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

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

Defined in Agda.Utils.Null

Methods

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

null :: (a, b, c, d) -> 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 #