Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 InstanceTable Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: InstanceTable Source # null :: InstanceTable -> 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 Signature Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: Signature Source # null :: Signature -> 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 (EnumSet a) Source # |
Instance details Defined in Agda.Utils.Null Methods empty :: EnumSet a Source # null :: EnumSet 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 (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 (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 (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 (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 (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 #

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

Disjunction (interpreting `null _` as `False`).