HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.Null

Overloaded null and empty for collections and sequences.

  • 1 class
  • 9 values
  • PackageAgda-2.7.0.1
  • Exports10
  • LanguageHaskell2010
  • LicenceMIT
  • SourceNull.hs
classclass Null a where
#

Methods

Instances85Null, …
  • Null RangeDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.Range
  • Null TypedBindingInfoDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract
  • Null WhereDeclarationsDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract
  • Null ExpandedEllipsisDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null FixityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null Fixity'Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null FixityLevelDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null HidingDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null Q0OriginDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null Q1OriginDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null QωOriginDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null KwRangeDefined in Agda-2.7.0.1 · Agda.Syntax.Common.KeywordRange
  • Null ExprInfoDefined in Agda-2.7.0.1 · Agda.Syntax.Info
  • Null LHSInfoDefined in Agda-2.7.0.1 · Agda.Syntax.Info
  • Null LetInfoDefined in Agda-2.7.0.1 · Agda.Syntax.Info
  • Null MetaInfoDefined in Agda-2.7.0.1 · Agda.Syntax.Info
  • Null MetaKindDefined in Agda-2.7.0.1 · Agda.Syntax.Info
  • Null MutualInfoDefined in Agda-2.7.0.1 · Agda.Syntax.Info

    Default value for MutualInfo.

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

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

  • Null ScopeDefined in Agda-2.7.0.1 · Agda.Syntax.Scope.Base
  • Null ScopeInfoDefined in Agda-2.7.0.1 · Agda.Syntax.Scope.Base
  • Null MetaSetDefined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
  • Null FieldsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
  • Null MutualBlockDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
  • Null ProjLamsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
  • Null SimplificationDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
  • Null OccurrenceDefined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity.Occurrence
  • Null NLMStateDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
  • Null LeftoverPatternsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
  • Null PermutationDefined in Agda-2.7.0.1 · Agda.Utils.Permutation
  • Null ProfileOptionsDefined in Agda-2.7.0.1 · Agda.Utils.ProfileOptions
  • Null ByteStringDefined in Agda-2.7.0.1 · Agda.Utils.Null
  • Null ByteStringDefined in Agda-2.7.0.1 · Agda.Utils.Null
  • Null IntSetDefined in Agda-2.7.0.1 · Agda.Utils.Null
  • Null BoolDefined in Agda-2.7.0.1 · Agda.Utils.Null

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

  • Null TextDefined in Agda-2.7.0.1 · Agda.Utils.Null
  • Null ()Defined in Agda-2.7.0.1 · Agda.Utils.Null
  • Null (RecordDirectives' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null (TacticAttribute' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete
  • Null (WhereClause' a)Defined in Agda-2.7.0.1 · 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.7.0.1 · Agda.Syntax.Internal
  • Null (Tele a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal
  • Null (Range' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Position
  • Null (AbsToCon Doc)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
  • Null (CallGraph cinfo)Defined in Agda-2.7.0.1 · Agda.Termination.CallGraph

    null checks whether the call graph is completely disconnected.

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

    Initial benchmark structure (empty).

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

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

  • Null (Doc a)Defined in Agda-2.7.0.1 · Agda.Utils.Null
  • Null (Maybe a)Defined in Agda-2.7.0.1 · Agda.Utils.Maybe.Strict · orphan
  • Null (HashSet a)Defined in Agda-2.7.0.1 · Agda.Utils.Null
  • Null [a]Defined in Agda-2.7.0.1 · Agda.Utils.Null
  • Null a => Null (Nice a)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Definitions.Monad
  • Null a => Null (SizedThing a)Defined in Agda-2.7.0.1 · Agda.Utils.Size
  • Null a => Null (Identity a)Defined in Agda-2.7.0.1 · Agda.Utils.Null
  • Null a => Null (IO a)Defined in Agda-2.7.0.1 · Agda.Utils.Null
  • SmallSetElement a => Null (SmallSet a)Defined in Agda-2.7.0.1 · Agda.Utils.SmallSet
  • Null (ImportDirective' n m)Defined in Agda-2.7.0.1 · 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.7.0.1 · Agda.Syntax.Common
  • Null (Solution rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.Syntax
  • Null (BiMap k v)Defined in Agda-2.7.0.1 · Agda.Utils.BiMap
  • Null (Trie k v)Defined in Agda-2.7.0.1 · Agda.Utils.Trie

    Empty trie.

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

    The null value of 'WithDefault b' is Default.

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

Testing for null.

9 declarations