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.Syntax.Common

Some common syntactic entities are defined in this module.

  • 79 types
  • 21 classes
  • 159 values
  • PackageAgda-2.7.0.1
  • Exports260
  • LanguageHaskell2010
  • LicenceMIT
  • SourceCommon.hs
datadata ImportDirective' n m
#

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

Constructors

Instances10Eq, Show, Semigroup, Monoid, NFData, Pretty, …
datadata Origin
#

Origin of arguments.

Constructors

  • UserWritten

    From the source file / user input. (Preserve!)

  • Inserted

    E.g. inserted hidden arguments.

  • Reflected

    Produced by the reflection machinery.

  • CaseSplit

    Produced by an interactive case split.

  • Substitution

    Named application produced to represent a substitution. E.g. "?0 (x = n)" instead of "?0 n"

  • ExpandedPun

    An expanded hidden argument pun.

  • Generalization

    Inserted by the generalization process

Instances9Eq, Ord, Show, NFData, HasRange, KillRange, …
  • Eq OriginDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Ord OriginDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Show OriginDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • NFData OriginDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • HasRange OriginDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • KillRange OriginDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • LensOrigin OriginDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • ChooseFlex OriginDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
  • EmbPrj OriginDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
newtypenewtype InteractionId
#

Constructors

Instances17Enum, Eq, Integral, Num, Ord, Read, …
datadata Modality
#

We have a tuple of modalities, which might not be fully orthogonal. For example, irrelevant stuff is also run-time irrelevant.

Constructors

  • Modality
    • modRelevance :: Relevance

      Legacy irrelevance. See Pfenning, LiCS 2001; Abel, Vezzosi and Winterhalter, ICFP 2017.

    • modQuantity :: Quantity

      Cardinality / runtime erasure. See Conor McBride, I got plenty o' nutting, Wadlerfest 2016. See Bob Atkey, Syntax and Semantics of Quantitative Type Theory, LiCS 2018.

    • modCohesion :: Cohesion

      Cohesion/what was in Agda-flat. see "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" (arXiv:1509.07584) Currently only the comonad is implemented.

Instances30Eq, Ord, Show, Generic, NFData, Pretty, …
newtypenewtype ProblemId
#

A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.

Constructors

Instances15Enum, Eq, Integral, Num, Ord, Real, …
datadata Fixity
#

Fixity of operators.

Constructors

Instances11Eq, Ord, Show, NFData, Pretty, HasRange, …
  • Eq FixityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Ord FixityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Show FixityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • NFData FixityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Pretty FixityDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Pretty · orphan
  • HasRange FixityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null FixityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • KillRange FixityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • LensFixity FixityDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • ToTerm FixityDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
  • EmbPrj FixityDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
datadata RewriteEqn' qn nm p e
#

RewriteEqn' qn p e represents the rewrite and irrefutable with clauses of the LHS. qn stands for the QName of the auxiliary function generated to implement the feature nm is the type of names for pattern variables p is the type of patterns e is the type of expressions

Constructors

Instances19Functor, Foldable, Traversable, Eq, Show, NFData, …
datadata MetaId
#

Meta-variable identifiers use the same structure as NameIds.

Constructors

Instances28Enum, Eq, Ord, Show, Generic, NFData, …
datadata Ranged a
#

Thing with range info.

Constructors

Instances41Functor, Foldable, Traversable, Decoration, MapNamedArgPattern, Eq, …
datadata Arg e
#

Constructors

Instances133Functor, Foldable, Traversable, Decoration, IsPrefixOf, MapNamedArgPattern, …
datadata ArgInfo
#

A function argument can be hidden and/or irrelevant.

Constructors

Instances23Eq, Ord, Show, NFData, HasRange, Hilite, …
datadata ConOrigin
#

Where does the ConP or Con come from?

Constructors

  • ConOSystem

    Inserted by system or expanded from an implicit pattern.

  • ConOCon

    User wrote a constructor (pattern).

  • ConORec

    User wrote a record (pattern).

  • ConOSplit

    Generated by interactive case splitting.

Instances10Bounded, Enum, Eq, Ord, Show, Generic, …
datadata Hiding
#

Constructors

Instances15Eq, Ord, Show, Semigroup, Monoid, NFData, …
classclass LensOrigin a where
#

A lens to access the Origin attribute in data structures. Minimal implementation: getOrigin and mapOrigin or LensArgInfo.

Methods

Instances8LensOrigin, …
datadata NameId
#

The unique identifier of a name. Second argument is the top-level module identifier.

Constructors

Instances14Enum, Eq, Ord, Show, Generic, NFData, …
datadata Named name a
#

Something potentially carrying a name.

Constructors

Instances76MapNamedArgPattern, PatternLike, Functor, Foldable, Traversable, Pretty, …
classclass LensHiding a where
#

A lens to access the Hiding attribute in data structures. Minimal implementation: getHiding and mapHiding or LensArgInfo.

Methods

Instances11LensHiding, …
datadata ProjOrigin
#

Where does a projection come from?

Constructors

Instances10Bounded, Enum, Eq, Ord, Show, Generic, …
datadata WithOrigin a
#

Decorating something with Origin information.

Constructors

Instances36Functor, Foldable, Traversable, Decoration, MapNamedArgPattern, Eq, …
datadata TerminationCheck m
#

Termination check? (Default = TerminationCheck).

Constructors

Instances5Functor, Eq, Show, NFData, KillRange
datadata Cohesion
#

Cohesion modalities see "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" (arXiv:1509.07584) types are now given an additional topological layer which the modalities interact with.

Constructors

  • Flat

    same points, discrete topology, idempotent comonad, box-like.

  • Continuous

    identity modality. | Sharp -- ^ same points, codiscrete topology, idempotent monad, diamond-like.

  • Squash

    single point space, artificially added for Flat left-composition.

Instances25Bounded, Enum, Eq, Ord, Show, Generic, …
datadata RecordDirectives' a
#

Constructors

Instances14Functor, Foldable, Traversable, ToConcrete, Hilite, DeclaredNames, …
  • Functor RecordDirectives'Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Foldable RecordDirectives'Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Traversable RecordDirectives'Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • ToConcrete RecordDirectivesDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
  • Hilite RecordDirectivesDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.FromAbstract

    Reengineered from the old Geniplate-implemented highlighting extraction. This was the old procedure:

    Traversal over declaration in abstract syntax that collects the following hiliting information:

    1. constructorInfo (highest prio)

    2.

    theRest

    (medium prio) 3.

    nameInfo

    (lowest prio)

    nameInfo: "All names mentioned in the syntax tree (not bound variables)." For each possibly ambiguous name (QName and AmbiguousQName) that not isExtendedLambdaName, do hiliteAmbiguous (used to be calledgenerate).

    constructorInfo (only when highlighting level == Full): "After the code has been type checked more information may be available for overloaded constructors, and generateConstructorInfo takes advantage of this information. Note, however, that highlighting for overloaded constructors is included also in nameInfo." This is not computed by recursion over the abstract syntax, but gets the constructor names stDisambiguatedNames that fall within the bounds of the current declaration.

    theRest: Bound variables, dotted patterns, record fields, module names, the "as" and "to" symbols and some other things.

    Here is a table what theRest used to collect:

    • -------------------------------------------------------------------- | A.Expr

    • -------------------------------------------------------------------- | getVarAndField (Expr) | A.Var | bound | getVarAndField | A.Rec(Update) | field | getExpr (Expr) | A.PatternSyn | patsyn | getExpr | A.Macro | macro

    • -------------------------------------------------------------------- | A.LetBinding

    • -------------------------------------------------------------------- | getLet | A.LetBind | bound | getLet | A.LetDeclaredVariable | bound

    • -------------------------------------------------------------------- | A.LamBinding

    • -------------------------------------------------------------------- | getLam | A.Binder under A.DomainFree | bound | getTyped | A.Binder under A.TBind | bound

    • -------------------------------------------------------------------- | A.Pattern'

    • -------------------------------------------------------------------- | getPattern(Syn) | A.VarP | bound | getPattern(Syn) | A.AsP | bound | getPattern(Syn) | A.DotP (not isProjP) | DottedPattern | getPattern(Syn) | A.RecP | field | getPattern(Syn) | A.PatternSynP | patsyn

    • -------------------------------------------------------------------- | A.Declaration

    • -------------------------------------------------------------------- | getFieldDecl | A.Field under A.RecDef | field | getPatSynArgs | A.PatternSynDef | bound | getPragma | A.BuiltinPragma... | keyword

    • -------------------------------------------------------------------- | A.NamedArg (polymorphism not supported in geniplate)

    • -------------------------------------------------------------------- | getNamedArg | NamedArg a | nameOf | getNamedArgE | NamedArg Exp | nameOf | getNamedArgP | NamedArg Pattern | nameOf | getNamedArgB | NamedArg BindName | nameOf | getNamedArgL | NamedArg LHSCore | nameOf

    | getModuleName | A.MName | mod | getModuleInfo | ModuleInfo | asName, (range of as,to) | getQuantityAttr | Common.Quantity | Symbol (if range)

  • DeclaredNames RecordDirectivesDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract.Views
  • Eq a => Eq (RecordDirectives' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Show a => Show (RecordDirectives' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • NFData a => NFData (RecordDirectives' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • HasRange a => HasRange (RecordDirectives' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Null (RecordDirectives' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • KillRange a => KillRange (RecordDirectives' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Common
  • EmbPrj a => EmbPrj (RecordDirectives' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan
  • type ConOfAbs RecordDirectives = [RecordDirective]Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
datadata Using' n m
#

The using clause of import directive.

Constructors

Instances10Eq, Show, Semigroup, Monoid, NFData, Pretty, …
datadata ImportedName' n m
#

An imported name can be a module or a defined name.

Constructors

Instances10Eq, Ord, Show, NFData, Pretty, HasRange, …
datadata Renaming' n m
#

Constructors

Instances7Eq, Show, NFData, Pretty, HasRange, Hilite, …
datadata Lock
#

Constructors

Instances9Eq, Ord, Show, Generic, NFData, Pretty, …
datadata Cubical
#

Variants of Cubical Agda.

CErasedCFull
Instances6Eq, Show, Generic, NFData, EmbPrj, Rep
datadata Language
#

Agda variants.

Only some variants are tracked.

Constructors

Instances7Eq, Show, Generic, NFData, KillRange, EmbPrj, …
datadata IsOpaque
#

Opaque or transparent.

Constructors

Instances10Eq, Ord, Show, Generic, NFData, KillRange, …
datadata Relevance
#

A function argument can be relevant or irrelevant. See Agda.TypeChecking.Irrelevance.

Constructors

  • Relevant

    The argument is (possibly) relevant at compile-time.

  • NonStrict

    The argument may never flow into evaluation position. Therefore, it is irrelevant at run-time. It is treated relevantly during equality checking.

    The above comment is probably obsolete, as we currently have erasure (at0, Quantity0) for that. What's described here is probably shape-irrelevance (..). If you enable --experimental-irrelevance, then the type of an irrelevant function is forced to be shape-irrelevant. See: - https://doi.org/10.2168/LMCS-8(1:29)2012 example 2.8 (Not enforcing shape-irrelevant codomains can break subject reduction!) - https://dl.acm.org/doi/10.1145/3110277 - https://doi.org/10.1145/3209108.3209119

  • Irrelevant

    The argument is irrelevant at compile- and runtime.

Instances27Bounded, Enum, Eq, Ord, Show, Generic, …
classclass LensRelevance a where
#

A lens to access the Relevance attribute in data structures. Minimal implementation: getRelevance and mapRelevance or LensModality.

Methods

Instances12LensRelevance, …
datadata WithHiding a
#

Decorating something with Hiding information.

Constructors

Instances30Functor, Applicative, Foldable, Traversable, Decoration, Eq, …
datadata OverlapMode
#

The possible overlap modes for an instance, also used for instance candidates.

Constructors

  • Overlappable

    User-written OVERLAPPABLE pragma: this candidate can *be removed* by a more specific candidate.

  • Overlapping

    User-written OVERLAPPING pragma: this candidate can *remove* a less specific candidate.

  • Overlaps

    User-written OVERLAPS pragma: both overlappable and overlapping.

  • DefaultOverlap

    No user-written overlap pragma. This instance can be overlapped by an OVERLAPPING instance, and it can overlap OVERLAPPABLE instances.

  • Incoherent

    User-written INCOHERENT pragma: both overlappable and overlapping; and, if there are multiple candidates after all overlap has been handled, make an arbitrary choice.

  • FieldOverlap

    Overlapping instances in record fields.

Instances10Bounded, Enum, Eq, Ord, Show, NFData, …
datadata Overlappable
#
YesOverlapNoOverlap
Instances6Eq, Ord, Show, Semigroup, Monoid, NFData
datadata Associativity
#

Associativity.

NonAssocLeftAssocRightAssoc
Instances6Eq, Ord, Show, Pretty, ToTerm, EmbPrj
datadata FileType
#
AgdaFileTypeMdFileTypeRstFileTypeTexFileTypeOrgFileTypeTypstFileType
Instances8Eq, Ord, Show, Generic, NFData, Pretty, …
datadata HasEta' a
#

Does a record come with eta-equality?

Constructors

Instances12Functor, Foldable, Traversable, CopatternMatchingAllowed, PatternMatchingAllowed, Eq, …
typetype HasEta = HasEta' PatternOrCopattern
#

Pattern and copattern matching is allowed in the presence of eta.

In the absence of eta, we have to choose whether we want to allow matching on the constructor or copattern matching with the projections. Having both leads to breakage of subject reduction (issue #4560).

datadata PatternOrCopattern
#

For a record without eta, which type of matching do we allow?

Constructors

Instances18Bounded, Enum, Eq, Ord, Show, NFData, …
classclass PatternMatchingAllowed a where
#

Can we pattern match on the record constructor?

Methods

Instances5PatternMatchingAllowed
classclass CopatternMatchingAllowed a where
#

Can we construct a record by copattern matching?

Methods

Instances5CopatternMatchingAllowed
classclass LensArgInfo a where
#

Methods

Instances5LensArgInfo
newtypenewtype UnderAddition t
#

Type wrapper to indicate additive monoid/semigroup context.

Constructors

Instances22Functor, Applicative, Eq, Ord, Show, Semigroup, …
newtypenewtype UnderComposition t
#

Type wrapper to indicate composition or multiplicative monoid/semigroup context.

Constructors

Instances27Functor, Applicative, Eq, Ord, Show, Semigroup, …
datadata Quantity
#

Quantity for linearity.

A quantity is a set of natural numbers, indicating possible semantic uses of a variable. A singleton set {n} requires that the corresponding variable is used exactly n times.

Constructors

Instances26Eq, Ord, Show, Generic, NFData, Pretty, …
valueinverseComposeModality :: Modality -> Modality -> Modality
#

inverseComposeModality r x returns the least modality y such that forall x, y we have x `moreUsableModality` (r `composeModality` y) iff (r `inverseComposeModality` x) `moreUsableModality` y (Galois connection).

classclass LensModality a where
#

Methods

Instances11LensModality, …
valueapplyModality :: LensModality a => Modality -> a -> a
#

Compose with modality flag from the left. This function is e.g. used to update the modality information on pattern variables a after a match against something of modality q.

valueinverseComposeRelevance :: Relevance -> Relevance -> Relevance
#

inverseComposeRelevance r x returns the most irrelevant y such that forall x, y we have x `moreRelevant` (r `composeRelevance` y) iff (r `inverseComposeRelevance` x) `moreRelevant` y (Galois connection).

valueinverseComposeQuantity :: Quantity -> Quantity -> Quantity
#

inverseComposeQuantity r x returns the least quantity y such that forall x, y we have x `moreQuantity` (r `composeQuantity` y) iff (r `inverseComposeQuantity` x) `moreQuantity` y (Galois connection).

valueinverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion
#

inverseComposeCohesion r x returns the least y such that forall x, y we have x `moreCohesion` (r `composeCohesion` y) iff (r `inverseComposeCohesion` x) `moreCohesion` y (Galois connection). The above law fails for r = Squash.

classclass LensQuantity a where
#

Methods

Instances11LensQuantity, …
datadata Q1Origin
#

Origin of Quantity1.

Constructors

Instances14Eq, Ord, Show, Generic, Semigroup, Monoid, …
valuedefaultModality :: Modality
#

The default Modality Beware that this is neither the additive unit nor the unit under composition, because the default quantity is ω.

valuedefaultQuantity :: Quantity
#

Absorptive element! This differs from Relevance and Cohesion whose default is the multiplicative unit.

classclass LensCohesion a where
#

A lens to access the Cohesion attribute in data structures. Minimal implementation: getCohesion and mapCohesion or LensModality.

Methods

Instances5LensCohesion
datadata Q0Origin
#

Origin of Quantity0.

Constructors

Instances14Eq, Ord, Show, Generic, Semigroup, Monoid, …
datadata QωOrigin
#

Origin of Quantityω.

Constructors

Instances14Eq, Ord, Show, Generic, Semigroup, Monoid, …
valueapplyQuantity :: LensQuantity a => Quantity -> a -> a
#

Compose with quantity flag from the left. This function is e.g. used to update the quantity information on pattern variables a after a match against something of quantity q.

datadata Erased
#

A special case of Quantity: erased or not.

Note that the Ord instance does *not* ignore the origin arguments.

Constructors

Instances12Eq, Ord, Show, Generic, NFData, Pretty, …
valueapplyRelevance :: LensRelevance a => Relevance -> a -> a
#

Compose with relevance flag from the left. This function is e.g. used to update the relevance information on pattern variables a after a match against something rel.

datadata Annotation
#

We have a tuple of annotations, which might not be fully orthogonal.

Constructors

  • Annotation
    • annLock :: Lock

      Fitch-style dependent right adjoints. See Modal Dependent Type Theory and Dependent Right Adjoints, arXiv:1804.05236.

Instances10Eq, Ord, Show, Generic, NFData, HasRange, …
datadata LockOrigin
#

Constructors

Instances7Bounded, Enum, Eq, Ord, Show, Generic, …
valueapplyCohesion :: LensCohesion a => Cohesion -> a -> a
#

Compose with cohesion flag from the left. This function is e.g. used to update the cohesion information on pattern variables a after a match against something of cohesion rel.

datadata FreeVariables
#

Constructors

Instances9Eq, Ord, Show, Semigroup, Monoid, NFData, …
classclass LensFreeVariables a where
#

A lens to access the FreeVariables attribute in data structures. Minimal implementation: getFreeVariables and mapFreeVariables or LensArgInfo.

Methods

Instances4LensFreeVariables
valuewithArgsFrom :: [a] -> [Arg b] -> [Arg a]
#

xs `withArgsFrom` args translates xs into a list of Args, using the elements in args to fill in the non-unArg fields.

Precondition: The two lists should have equal length.

familytype family NameOf a
#

The type of the name

Instances4NameOf
  • type NameOf (Arg a) = NameOf aDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • type NameOf (Named name a) = nameDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • type NameOf (Dom' t e) = NamedNameDefined in Agda-2.7.0.1 · Agda.Syntax.Internal
  • type NameOf (Maybe a) = aDefined in Agda-2.7.0.1 · Agda.Syntax.Common
datadata IsInfix
#

Functions can be defined in both infix and prefix style. See LHS.

InfixDefPrefixDef
Instances3Eq, Ord, Show
  • Eq IsInfixDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Ord IsInfixDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Show IsInfixDefined in Agda-2.7.0.1 · Agda.Syntax.Common
datadata Access
#

Access modifier.

Constructors

Instances9Eq, Ord, Show, NFData, Pretty, HasRange, …
  • Eq AccessDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Ord AccessDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Show AccessDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • NFData AccessDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • Pretty AccessDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • HasRange AccessDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • KillRange AccessDefined in Agda-2.7.0.1 · Agda.Syntax.Common
  • MakePrivate AccessDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Definitions
  • EmbPrj AccessDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Abstract · orphan
datadata IsAbstract
#

Abstract or concrete.

AbstractDefConcreteDef
Instances15Eq, Ord, Show, Generic, Semigroup, Monoid, …
datadata IsInstance
#

Is this definition eligible for instance search?

Constructors

Instances7Eq, Ord, Show, NFData, HasRange, KillRange, …
datadata IsMacro
#

Is this a macro definition?

MacroDefNotMacroDef
Instances8Eq, Ord, Show, Generic, NFData, HasRange, …
datadata OpaqueId
#

The unique identifier of an opaque block. Second argument is the top-level module identifier.

Constructors

Instances12Enum, Eq, Ord, Show, Generic, NFData, …
datadata PositionInName
#

The position of a name part or underscore in a name.

Constructors

  • Beginning

    The following underscore is at the beginning of the name: _foo.

  • Middle

    The following underscore is in the middle of the name: foo_bar.

  • End

    The following underscore is at the end of the name: foo_.

Instances3Eq, Ord, Show
datadata MaybePlaceholder e
#

Placeholders are used to represent the underscores in a section.

Constructors

Instances11Functor, Foldable, Traversable, Eq, Ord, Show, …
datadata FixityLevel
#

Constructors

Instances8Eq, Ord, Show, NFData, Pretty, Null, …
datadata Fixity'
#

The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.

Constructors

Instances12Eq, Show, NFData, Pretty, Null, KillRange, …
classclass LensFixity a where
#

Methods

Instances7LensFixity, …
datadata PositivityCheck
#

Positivity check? (Default = True).

YesPositivityCheckNoPositivityCheck
Instances11Bounded, Enum, Eq, Ord, Show, Generic, …
datadata UniverseCheck
#

Universe check? (Default is yes).

YesUniverseCheckNoUniverseCheck
Instances9Bounded, Enum, Eq, Ord, Show, Generic, …
datadata CoverageCheck
#

Coverage check? (Default is yes).

YesCoverageCheckNoCoverageCheck
Instances11Bounded, Enum, Eq, Ord, Show, Generic, …
datadata ExpandedEllipsis
#

Constructors

Instances8Eq, Show, Semigroup, Monoid, NFData, Null, …
datadata NotationPart
#

Notation parts.

Constructors

  • IdPart RString

    An identifier part. For instance, for _+_ the only identifier part is +.

  • HolePart Range (NamedArg (Ranged Int))

    A hole: a place where argument expressions can be written. For instance, for _+_ the two underscores are holes, and for syntax Σ A (λ x → B) = B , A , x the variables A and B are holes. The number is the position of the hole, counting from zero. For instance, the number for A is 0, and the number for B is 1.

  • VarPart Range (Ranged BoundVariablePosition)

    A bound variable.

    The first range is the range of the variable in the right-hand side of the syntax declaration, and the second range is the range of the variable in the left-hand side.

  • WildPart (Ranged BoundVariablePosition)

    A wildcard (an underscore in binding position).

Instances9Eq, Ord, Show, NFData, Pretty, HasRange, …
datadata BoundVariablePosition
#

Positions of variables in syntax declarations.

Constructors

  • BoundVariablePosition
    • holeNumber :: !Int

      The position (in the left-hand side of the syntax declaration) of the hole in which the variable is bound, counting from zero (and excluding parts that are not holes). For instance, for syntax Σ A (λ x → B) = B , A , x the number for x is 1, corresponding to B (0 would correspond to A).

    • varNumber :: !Int

      The position in the list of variables for this particular variable, counting from zero, and including wildcards. For instance, for syntax F (λ x _ y → A) = y ! A ! x the number for x is 0, the number for _ is 1, and the number for y is 2.

Instances5Eq, Ord, Show, NFData, EmbPrj

module Agda.Syntax.Common.KeywordRange

module Agda.Syntax.TopLevelModuleName.Boot

datadata Induction
#
InductiveCoInductive
Instances9Eq, Ord, Show, NFData, Pretty, HasRange, …

Orphan instances

3 instances