Safe Haskell	Safe-Inferred
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 ()

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 Methods empty :: Range Source # null :: Range -> Bool Source #
Null WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods empty :: WhereDeclarations Source # null :: WhereDeclarations -> 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 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 Methods empty :: QωOrigin Source # null :: QωOrigin -> 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 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 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 Occurrence Source #
Instance details Defined in Agda.TypeChecking.Positivity.Occurrence Methods empty :: Occurrence Source # null :: Occurrence -> 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 Permutation Source #
Instance details Defined in Agda.Utils.Permutation Methods empty :: Permutation Source # null :: Permutation -> 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 Doc Source #
Instance details Defined in Agda.Utils.Null Methods empty :: Doc Source # null :: Doc -> 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 (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 (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 (AbsToCon Doc) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods empty :: AbsToCon Doc Source # null :: AbsToCon Doc -> 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 (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 #
Null a => Null (Identity a) Source #
Instance details Defined in Agda.Utils.Null Methods empty :: Identity a Source # null :: Identity 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 (IO a) Source #
Instance details Defined in Agda.Utils.Null Methods empty :: IO a Source # null :: IO 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 (HashSet a) Source #
Instance details Defined in Agda.Utils.Null Methods empty :: HashSet a Source # null :: HashSet 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 (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 (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 #