Safe Haskell	None
Language	Haskell2010

Agda.Utils.Null

Contents

Testing for null.

Description

Overloaded null and empty for collections and sequences.

Synopsis

class Null a where
- empty :: a
- null :: a -> Bool
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 ()
applyUnlessNull :: Null a => a -> (a -> b -> b) -> b -> b
catchNull :: Null a => a -> a -> a

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 LibCache Source #
Instance details Defined in Agda.Interaction.Library.Base Methods empty :: LibCache Source # null :: LibCache -> Bool Source #
Null LibName Source #
Instance details Defined in Agda.Interaction.Library.Base Methods empty :: LibName Source # null :: LibName -> Bool Source #
Null TypedBindingInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods empty :: TypedBindingInfo Source # null :: TypedBindingInfo -> Bool Source #
Null WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods empty :: WhereDeclarations Source # null :: WhereDeclarations -> Bool Source #
Null ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods empty :: ModuleName Source # null :: ModuleName -> Bool Source #
Null Suffix Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods empty :: Suffix Source # null :: Suffix -> Bool Source #
Null Annotation Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Annotation Source # null :: Annotation -> Bool Source #
Null ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: ArgInfo Source # null :: ArgInfo -> Bool Source #
Null Catchall Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Catchall Source # null :: Catchall -> Bool Source #
Null Cohesion Source #	`null` shall mean no information, not even origin or range.
Instance details Defined in Agda.Syntax.Common Methods empty :: Cohesion Source # null :: Cohesion -> Bool Source #
Null ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: ExpandedEllipsis Source # null :: ExpandedEllipsis -> Bool Source #
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 Methods empty :: FixityLevel Source # null :: FixityLevel -> Bool Source #
Null Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Hiding Source # null :: Hiding -> Bool Source #
Null Lock Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Lock Source # null :: Lock -> Bool Source #
Null Modality Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Modality Source # null :: Modality -> Bool Source #
Null OriginIrrelevant Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: OriginIrrelevant Source # null :: OriginIrrelevant -> Bool Source #
Null OriginRelevant Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: OriginRelevant Source # null :: OriginRelevant -> Bool Source #
Null OriginShapeIrrelevant Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: OriginShapeIrrelevant Source # null :: OriginShapeIrrelevant -> Bool Source #
Null PolarityModality Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: PolarityModality Source # null :: PolarityModality -> 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 Quantity Source #	`null` means no information, not even origin or range.
Instance details Defined in Agda.Syntax.Common Methods empty :: Quantity Source # null :: Quantity -> Bool Source #
Null QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: QωOrigin Source # null :: QωOrigin -> Bool Source #
Null Relevance Source #	`null` means no information, not even origin or range.
Instance details Defined in Agda.Syntax.Common Methods empty :: Relevance Source # null :: Relevance -> Bool Source #
Null KwRange Source #
Instance details Defined in Agda.Syntax.Common.KeywordRange Methods empty :: KwRange Source # null :: KwRange -> Bool Source #
Null WhereClause_ Source #
Instance details Defined in Agda.Syntax.Concrete Methods empty :: WhereClause_ Source # null :: WhereClause_ -> Bool Source #
Null AppInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: AppInfo Source # null :: AppInfo -> 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 Methods empty :: MutualInfo Source # null :: MutualInfo -> Bool Source #
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 Methods empty :: ScopeInfo Source # null :: ScopeInfo -> Bool Source #
Null GuardednessHelps Source #
Instance details Defined in Agda.Termination.Termination Methods empty :: GuardednessHelps Source # null :: GuardednessHelps -> Bool Source #
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 Methods empty :: MutualBlock Source # null :: MutualBlock -> Bool Source #
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 Methods empty :: Simplification Source # null :: Simplification -> Bool Source #
Null WarningsAndNonFatalErrors Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: WarningsAndNonFatalErrors Source # null :: WarningsAndNonFatalErrors -> Bool Source #
Null Occurrence Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods empty :: Occurrence Source # null :: Occurrence -> Bool Source #
Null OccursWhere Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods empty :: OccursWhere Source # null :: OccursWhere -> Bool Source #
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 Methods empty :: LeftoverPatterns Source # null :: LeftoverPatterns -> Bool Source #
Null FileDict Source #
Instance details Defined in Agda.Utils.FileId Methods empty :: FileDict Source # null :: FileDict -> Bool Source #
Null FileDictBuilder Source #
Instance details Defined in Agda.Utils.FileId Methods empty :: FileDictBuilder Source # null :: FileDictBuilder -> Bool Source #
Null Permutation Source #
Instance details Defined in Agda.Utils.Permutation Methods empty :: Permutation Source # null :: Permutation -> Bool Source #
Null ProfileOptions Source #
Instance details Defined in Agda.Utils.ProfileOptions Methods empty :: ProfileOptions Source # null :: ProfileOptions -> Bool Source #
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 a => Null (RecordDirectives' a) Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: RecordDirectives' a Source # null :: RecordDirectives' a -> Bool Source #
Null (TacticAttribute' a) Source #
Instance details Defined in Agda.Syntax.Concrete Methods empty :: TacticAttribute' a Source # null :: TacticAttribute' a -> Bool Source #
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 Methods empty :: WhereClause' a Source # null :: WhereClause' a -> Bool Source #
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 Methods empty :: Substitution' a Source # null :: Substitution' a -> Bool Source #
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 (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 (EnumSet a) Source #
Instance details Defined in Agda.Utils.Null Methods empty :: EnumSet a Source # null :: EnumSet 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 Methods empty :: ImportDirective' n m Source # null :: ImportDirective' n m -> 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 #
Monad m => Null (PureConversionT m Doc) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods empty :: PureConversionT m Doc Source # null :: PureConversionT m Doc -> Bool Source #
(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 (Boundary' x a) Source #
Instance details Defined in Agda.TypeChecking.Telescope Methods empty :: Boundary' x a Source # null :: Boundary' x a -> 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 (EnumMap k a) Source #
Instance details Defined in Agda.Utils.Null Methods empty :: EnumMap k a Source # null :: EnumMap 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 (m a), Monad m) => Null (MaybeT m a) Source #
Instance details Defined in Agda.Utils.Null Methods empty :: MaybeT m a Source # null :: MaybeT m 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 #

catchNull :: Null a => a -> a -> a Source #

Disjunction (interpreting null _ as False).