HORIZON HASKELLDocslts/ghc-10.0.xfc4e5982026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 10.0.0.20260917 · lts/ghc-10.0.x · fc4e598 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Null

Overloaded null and empty for collections and sequences.

  • 1 class
  • 10 values
  • PackageAgda-2.8.0.2
  • Exports11
  • LanguageHaskell2010
  • LicenceMIT
  • SourceNull.hs
classclass Null a where
#

Methods

Instances114Null, …
  • Null RangeDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.Range
  • Null LibCacheDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
  • Null LibNameDefined in Agda-2.8.0.2 · Agda.Interaction.Library.Base
  • Null TypedBindingInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
  • Null WhereDeclarationsDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
  • Null ModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
  • Null SuffixDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
  • Null AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null CatchallDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common

    null shall mean no information, not even origin or range.

  • Null ExpandedEllipsisDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null FixityLevelDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null LockDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common

    null means no information, not even origin or range.

  • Null RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common

    null means no information, not even origin or range.

  • Null KwRangeDefined in Agda-2.8.0.2 · Agda.Syntax.Common.KeywordRange
  • Null WhereClause_Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete
  • Null AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
  • Null ExprInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
  • Null LHSInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
  • Null LetInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
  • Null MetaInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
  • Null MetaKindDefined in Agda-2.8.0.2 · Agda.Syntax.Info
  • Null MutualInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info

    Default value for MutualInfo.

  • Null PatInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
  • Null ClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Internal

    A null clause is one with no patterns and no rhs. Should not exist in practice.

  • Null ScopeDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Base
  • Null ScopeInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Base
  • Null GuardednessHelpsDefined in Agda-2.8.0.2 · Agda.Termination.Termination
  • Null MetaSetDefined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy
  • Null FieldsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Null InstanceTableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Null MutualBlockDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Null ProjLamsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Null SignatureDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Null SimplificationDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Null WarningsAndNonFatalErrorsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Null OccurrenceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity.Occurrence
  • Null OccursWhereDefined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity.Occurrence
  • Null NLMStateDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinMatch
  • Null LeftoverPatternsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
  • Null FileDictDefined in Agda-2.8.0.2 · Agda.Utils.FileId
  • Null FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileId
  • Null PermutationDefined in Agda-2.8.0.2 · Agda.Utils.Permutation
  • Null ProfileOptionsDefined in Agda-2.8.0.2 · Agda.Utils.ProfileOptions
  • Null ByteStringDefined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null ByteStringDefined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null IntSetDefined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null BoolDefined in Agda-2.8.0.2 · Agda.Utils.Null

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

  • Null TextDefined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null ()Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null (TacticAttribute' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete
  • Null (WhereClause' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete

    A WhereClause is null when the where keyword is absent. An empty list of declarations does not count as null here.

  • Null (Substitution' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
  • Null (Tele a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
  • Null (Range' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Position
  • Null (CallGraph cinfo)Defined in Agda-2.8.0.2 · Agda.Termination.CallGraph

    null checks whether the call graph is completely disconnected.

  • Null (CMSet cinfo)Defined in Agda-2.8.0.2 · Agda.Termination.CallMatrix
  • Null (Case m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.CompiledClause
  • Null (DiscrimTree a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.DiscrimTree.Types
  • Null (TCM Doc)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • Null (Match a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.Match
  • Null (Bag a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null (Benchmark a)Defined in Agda-2.8.0.2 · Agda.Utils.Benchmark

    Initial benchmark structure (empty).

  • Null (Favorites a)Defined in Agda-2.8.0.2 · Agda.Utils.Favorites
  • Null (RangeMap a)Defined in Agda-2.8.0.2 · Agda.Utils.RangeMap
  • Null (IntMap a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null (Seq a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null (Set a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null (EnumSet a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null (Maybe a)Defined in Agda-2.8.0.2 · Agda.Utils.Null

    A Maybe is null when it corresponds to the empty list.

  • Null (Doc a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null (Maybe a)Defined in Agda-2.8.0.2 · Agda.Utils.Maybe.Strict · orphan
  • Null (HashSet a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null [a]Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null a => Null (RecordDirectives' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null a => Null (Nice a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions.Monad
  • Null a => Null (SizedThing a)Defined in Agda-2.8.0.2 · Agda.Utils.Size
  • Null a => Null (Identity a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null a => Null (IO a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • SmallSetElement a => Null (SmallSet a)Defined in Agda-2.8.0.2 · Agda.Utils.SmallSet
  • Null (ImportDirective' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

    null for import directives holds when everything is imported unchanged (no names are hidden or renamed).

  • Null (Using' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
  • Null (Solution rigid flex)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SizedTypes.Syntax
  • Null (Boundary' x a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Telescope
  • Null (BiMap k v)Defined in Agda-2.8.0.2 · Agda.Utils.BiMap
  • Null (Trie k v)Defined in Agda-2.8.0.2 · Agda.Utils.Trie

    Empty trie.

  • Null (WithDefault' a b)Defined in Agda-2.8.0.2 · Agda.Utils.WithDefault

    The null value of 'WithDefault b' is Default.

  • Null (Map k a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null (EnumMap k a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Null (HashMap k a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • Monad m => Null (PureConversionT m Doc)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure
  • (Null (m a), Monad m) => Null (MaybeT m a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • (Null a, Null b) => Null (a, b)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • (Monad m, Null (m Doc)) => Null (AbsToConT m Doc)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
  • (MonadIO m, Null a) => Null (TCMT m a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
  • (Null (m a), Monad m) => Null (ExceptT e m a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • (Null (m a), Monad m) => Null (ReaderT r m a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • (Null (m a), Monad m) => Null (StateT s m a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • (Null (m a), Monad m, Monoid w) => Null (WriterT w m a)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • (Null a, Null b, Null c) => Null (a, b, c)Defined in Agda-2.8.0.2 · Agda.Utils.Null
  • (Null a, Null b, Null c, Null d) => Null (a, b, c, d)Defined in Agda-2.8.0.2 · Agda.Utils.Null

Testing for null.

10 declarations
valuecatchNull :: Null a => a -> a -> a
#

Disjunction (interpreting null _ as False).