Agda-2.6.20240714: 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 #

The default implementation of null compares with empty, first trying pointer equality, then falling back to Eq equality.

Instances

Instances details
Null Range Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Range

Methods

empty :: Range Source #

null :: Range -> Bool Source #

Null TypedBindingInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

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

Methods

empty :: Fixity Source #

null :: Fixity -> Bool Source #

Null Fixity' Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Fixity' Source #

null :: Fixity' -> Bool Source #

Null FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Common

Null Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Hiding Source #

null :: Hiding -> Bool Source #

Null Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Q0Origin Source #

null :: Q0Origin -> Bool Source #

Null Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

empty :: Q1Origin Source #

null :: Q1Origin -> Bool Source #

Null QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Common

Null KwRange Source # 
Instance details

Defined in Agda.Syntax.Common.KeywordRange

Methods

empty :: KwRange Source #

null :: KwRange -> Bool Source #

Null ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: ExprInfo Source #

null :: ExprInfo -> Bool Source #

Null LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: LHSInfo Source #

null :: LHSInfo -> Bool Source #

Null LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: LetInfo Source #

null :: LetInfo -> Bool Source #

Null MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: MetaInfo Source #

null :: MetaInfo -> Bool Source #

Null MetaKind Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: MetaKind Source #

null :: MetaKind -> Bool Source #

Null MutualInfo Source #

Default value for MutualInfo.

Instance details

Defined in Agda.Syntax.Info

Null PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: PatInfo Source #

null :: PatInfo -> Bool Source #

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

Methods

empty :: Clause Source #

null :: Clause -> Bool Source #

Null Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

empty :: Scope Source #

null :: Scope -> Bool Source #

Null ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Null MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

empty :: MetaSet Source #

null :: MetaSet -> Bool Source #

Null Fields Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: Fields Source #

null :: Fields -> Bool Source #

Null MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: ProjLams Source #

null :: ProjLams -> Bool Source #

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

Methods

empty :: NLMState Source #

null :: NLMState -> Bool Source #

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

Methods

empty :: ByteString Source #

null :: ByteString -> Bool Source #

Null ByteString Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: ByteString Source #

null :: ByteString -> Bool Source #

Null IntSet Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: IntSet Source #

null :: IntSet -> Bool Source #

Null Text Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: Text Source #

null :: Text -> Bool Source #

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

Methods

empty :: Bool Source #

null :: Bool -> Bool Source #

Null (RecordDirectives' a) Source # 
Instance details

Defined in Agda.Syntax.Common

Null (TacticAttribute' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete

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

Defined in Agda.TypeChecking.DiscrimTree.Types

Methods

empty :: DiscrimTree a Source #

null :: DiscrimTree a -> Bool Source #

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCM Doc Source #

null :: TCM Doc -> Bool Source #

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

Methods

empty :: Benchmark a Source #

null :: Benchmark a -> Bool Source #

Null (Favorites a) Source # 
Instance details

Defined in Agda.Utils.Favorites

Methods

empty :: Favorites a Source #

null :: Favorites a -> Bool Source #

Null (RangeMap a) Source # 
Instance details

Defined in Agda.Utils.RangeMap

Methods

empty :: RangeMap a Source #

null :: RangeMap a -> Bool Source #

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

Defined in Agda.Utils.Size

Methods

empty :: SizedThing a Source #

null :: SizedThing a -> Bool Source #

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

Defined in Agda.Utils.SmallSet

Methods

empty :: SmallSet a Source #

null :: SmallSet 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 a => Null (Identity a) Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: Identity a Source #

null :: Identity 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

Methods

empty :: WithDefault' a b Source #

null :: WithDefault' 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 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 #

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