ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Common

Some common syntactic entities are defined in this module.

91 types
22 classes
198 values

PackageAgda-2.8.0.2
Exports312
LanguageHaskell2010
LicenceMIT
SourceCommon.hs

value_fixityAssoc :: Lens' Fixity Associativity

value_fixityLevel :: Lens' Fixity FixityLevel

valueaddCohesion :: Cohesion -> Cohesion -> Cohesion

Combine inferred Cohesion. The unit is Squash.

valueaddModality :: Modality -> Modality -> Modality

Modality forms a pointwise additive monoid.

valueaddPolarity :: PolarityModality -> PolarityModality -> PolarityModality

Combine inferred PolarityModality.

valueaddPolarity' :: ModalPolarity -> ModalPolarity -> ModalPolarity

Combine inferred ModalPolarity. The unit is UnusedPolarity.

valueaddQuantity :: Quantity -> Quantity -> Quantity

Quantity forms an additive monoid with zero Quantity0.

valueaddRelevance :: Relevance -> Relevance -> Relevance

Combine inferred Relevance. The unit is Irrelevant.

valueallCohesions :: [Cohesion]

valueallModalPolarities :: [ModalPolarity]

valueappendArgNames :: ArgName -> ArgName -> ArgName

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.

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.

valueapplyPolarity :: LensModalPolarity a => PolarityModality -> a -> a

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

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.

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.

valueargNameToString :: ArgName -> String

valueasQuantity :: Erased -> Quantity

Erased can be embedded into Quantity.

valuebareNameOf :: (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName

valuebareNameWithDefault

:: (LensNamed a, NameOf a ~ NamedName)
=> ArgName
-> a
-> ArgName

valuebestConInfo :: ConOrigin -> ConOrigin -> ConOrigin

Prefer user-written over system-inserted.

valuecomposeCohesion :: Cohesion -> Cohesion -> Cohesion

Cohesion composition. Squash is dominant, Continuous is neutral.

valuecomposeErased :: Erased -> Erased -> Erased

Composition of values of type Erased.

Erased is dominant. NotErased is neutral.

Right-biased for the origin.

valuecomposeModality :: Modality -> Modality -> Modality

Multiplicative monoid (standard monoid).

valuecomposePolarity :: PolarityModality -> PolarityModality -> PolarityModality

PolarityModality composition.

valuecomposePolarity' :: ModalPolarity -> ModalPolarity -> ModalPolarity

ModalPolarity composition. UnusedPolarity is dominant, StrictlyPositive is neutral.

valuecomposeQuantity :: Quantity -> Quantity -> Quantity

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

valuecomposeRelevance :: Relevance -> Relevance -> Relevance

Relevance composition. Irrelevant is dominant, Relevant is neutral. Composition coincides with max.

valuecubicalOptionString :: Cubical -> String

valuedefaultAnnotation :: Annotation

valuedefaultArg :: a -> Arg a

valuedefaultArgInfo :: ArgInfo

valuedefaultCheckModality :: Modality

The default Modality terms are checked against.

valuedefaultCohesion :: Cohesion

Default Cohesion is the identity element under composition

valuedefaultErased :: Erased

The default value of type Erased: not erased.

valuedefaultFixity :: Fixity

valuedefaultImportDir :: ImportDirective' n m

Default is directive is private (use everything, but do not export).

valuedefaultIrrelevantArgInfo :: ArgInfo

valuedefaultLock :: Lock

valuedefaultModality :: Modality

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

valuedefaultNamedArg :: a -> NamedArg a

valuedefaultPolarity :: PolarityModality

Default used when not caring about polarity

valuedefaultQuantity :: Quantity

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

valuedefaultRelevance :: Relevance

Default Relevance is the identity element under composition

valueemptyRecordDirectives :: Null a => RecordDirectives' a

valueerasedFromQuantity :: Quantity -> Maybe Erased

Quantity can be projected onto Erased.

valuefittingNamedArg

:: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, LensHiding dom)
=> arg
-> dom
-> Maybe Bool

Does an argument arg fit the shape dom of the next expected argument?

The hiding has to match, and if the argument has a name, it should match the name of the domain.

Nothing should be __IMPOSSIBLE__, so use as @fromMaybe IMPOSSIBLE $ fittingNamedArg arg dom@

valuefreeVariablesFromList :: [Int] -> FreeVariables

valuefromImportedName :: ImportedName' a a -> a

valuegetCohesionMod :: LensModality a => LensGet a Cohesion

valuegetFreeVariablesArgInfo :: LensArgInfo a => LensGet a FreeVariables

valuegetHidingArgInfo :: LensArgInfo a => LensGet a Hiding

valuegetModalityArgInfo :: LensArgInfo a => LensGet a Modality

valuegetNameOf :: LensNamed a => a -> Maybe (NameOf a)

valuegetOriginArgInfo :: LensArgInfo a => LensGet a Origin

valuegetPolarityMod :: LensModality a => LensGet a PolarityModality

valuegetQuantityMod :: LensModality a => LensGet a Quantity

valuegetRelevanceMod :: LensModality a => LensGet a Relevance

valuehasNoFreeVariables :: LensFreeVariables a => a -> Bool

valuehasQuantity0 :: LensQuantity a => a -> Bool

Check for Quantity0.

valuehasQuantity1 :: LensQuantity a => a -> Bool

Check for Quantity1.

valuehasQuantityω :: LensQuantity a => a -> Bool

Check for Quantityω.

valuehidden :: LensHiding a => a -> Bool

Hidden arguments are hidden.

valuehide :: LensHiding a => a -> a

valuehideOrKeepInstance :: LensHiding a => a -> a

valuehidingToString :: Hiding -> String

valueinverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a

Left division by a Cohesion. Used e.g. to modify context when going into a rel argument.

valueinverseApplyModalityButNotQuantity :: LensModality a => Modality -> a -> a

Left division by a Modality. Used e.g. to modify context when going into a m argument.

Note that this function does not change quantities.

valueinverseApplyPolarity :: LensModalPolarity a => PolarityModality -> a -> a

Left division by a PolarityModality. Used e.g. to modify context when going into a pol argument.

valueinverseApplyQuantity :: LensQuantity a => Quantity -> a -> a

Left division by a Quantity. Used e.g. to modify context when going into a q argument.

valueinverseApplyRelevance :: LensRelevance a => Relevance -> a -> a

Left division by a Relevance. Used e.g. to modify context when going into a rel argument.

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.

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).

valueinverseComposePolarity

:: PolarityModality
-> PolarityModality
-> PolarityModality

inverseComposePolarity r x returns the least y such that forall x, y we have x `morePolarity\ (r `composePolarity` y) iff (r `inverseComposePolarity` x) `morePolarity\ y (Galois connection).

valueinverseComposePolarity' :: ModalPolarity -> ModalPolarity -> ModalPolarity

inverseComposePolarity r x returns the least y such that forall x, y we have x `morePolarity\ (r `composePolarity` y) iff (r `inverseComposePolarity` x) `morePolarity\ 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).

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).

valueirrelevant :: Relevance

valueirrelevantToShapeIrrelevant :: Relevance -> Relevance

Irrelevant function arguments may appear non-strictly in the codomain type.

valueisContinuous :: LensCohesion a => a -> Bool

valueisDefaultImportDir :: ImportDirective' n m -> Bool

isDefaultImportDir implies null, but not the other way round.

valueisErased :: Erased -> Bool

Is the value "erased"?

valueisIncoherent :: HasOverlapMode a => a -> Bool

valueisInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool

valueisInstance :: LensHiding a => a -> Bool

valueisIrrelevant :: LensRelevance a => a -> Bool

valueisOverlappable :: HasOverlapMode a => a -> Bool

valueisOverlapping :: HasOverlapMode a => a -> Bool

valueisQuantity0 :: LensQuantity a => a -> Bool

valueisQuantityω :: LensQuantity a => a -> Bool

valueisRelevant :: LensRelevance a => a -> Bool

valueisShapeIrrelevant :: LensRelevance a => a -> Bool

valueisUnnamed :: Named name a -> Maybe a

valueisYesOverlap :: LensHiding a => a -> Bool

valuelModCohesion :: Lens' Modality Cohesion

valuelModPolarity :: Lens' Modality PolarityModality

valuelModQuantity :: Lens' Modality Quantity

valuelModRelevance :: Lens' Modality Relevance

valuemakeInstance :: LensHiding a => a -> a

valuemakeInstance' :: LensHiding a => Overlappable -> a -> a

valuemapCohesionMod :: LensModality a => LensMap a Cohesion

valuemapFreeVariablesArgInfo :: LensArgInfo a => LensMap a FreeVariables

valuemapHidingArgInfo :: LensArgInfo a => LensMap a Hiding

valuemapModalityArgInfo :: LensArgInfo a => LensMap a Modality

valuemapNameOf :: LensNamed a => (Maybe (NameOf a) -> Maybe (NameOf a)) -> a -> a

valuemapOriginArgInfo :: LensArgInfo a => LensMap a Origin

valuemapPolarityMod :: LensModality a => LensMap a PolarityModality

valuemapQuantityMod :: LensModality a => LensMap a Quantity

valuemapRelevanceMod :: LensModality a => LensMap a Relevance

valuemapUsing

:: [ImportedName' n1 m1] -> [ImportedName' n2 m2]
-> Using' n1 m1
-> Using' n2 m2

valuemergeHiding :: LensHiding a => WithHiding a -> a

Monoidal composition of Hiding information in some data.

valuemixedPolarity :: PolarityModality

Alias for Mixed polarity.

valuemoreCohesion :: Cohesion -> Cohesion -> Bool

Information ordering. Flat `moreCohesion` Continuous `moreCohesion` Sharp `moreCohesion` Squash

valuemorePolarity :: PolarityModality -> PolarityModality -> Bool

valuemorePolarity' :: ModalPolarity -> ModalPolarity -> Bool

morePolarity' x y is True whenever a variable of polarity x can be used anywhere where a variable of polarity y is expected. Note that morePolarity' x y actually means x <= y.

valuemoreQuantity :: Quantity -> Quantity -> Bool

m moreUsableQuantity m' means that an m can be used where ever an m' is required.

valuemoreRelevant :: Relevance -> Relevance -> Bool

Information ordering. Relevant `moreRelevant` ShapeIrrelevant `moreRelevant` Irrelevant

valuemoreUsableModality :: Modality -> Modality -> Bool

m moreUsableModality m' means that an m can be used where ever an m' is required.

valuenamed :: name -> a -> Named name a

valuenamedArg :: NamedArg a -> a

Get the content of a NamedArg.

valuenamedSame

:: (LensNamed a, LensNamed b, NameOf a ~ NamedName, NameOf b ~ NamedName)
=> a
-> b
-> Bool

Equality of argument names of things modulo Range and Origin.

valuenegativePolarity :: PolarityModality

Alias for Negative polarity.

valuenoFixity :: Fixity

valuenoFixity' :: Fixity'

valuenoFreeVariables :: FreeVariables

valuenoNotation :: Notation

valuenoPlaceholder :: e -> MaybePlaceholder e

An abbreviation: noPlaceholder = NoPlaceholder Nothing.

valuenoUserQuantity :: LensQuantity a => a -> Bool

Did the user supply a quantity annotation?

valuenotVisible :: LensHiding a => a -> Bool

Instance and Hidden arguments are notVisible.

valueoneFreeVariable :: Int -> FreeVariables

valuepartitionImportedNames :: [ImportedName' n m] -> ([n], [m])

Like partitionEithers.

valuepositionalModalityComponent :: Modality -> Modality

Extract the positional modality component for checks regarding only them.

valueprettyCohesion :: LensCohesion a => a -> Doc -> Doc

valueprettyErased :: Erased -> Doc -> Doc

valueprettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc

prettyHiding info visible doc puts the correct braces around doc according to info info and returns visible doc if the we deal with a visible thing.

valueprettyLock :: LensLock a => a -> Doc -> Doc

valueprettyPolarity :: LensModalPolarity a => a -> Doc -> Doc

valueprettyQuantity :: LensQuantity a => a -> Doc -> Doc

valueprettyRelevance :: LensRelevance a => a -> Doc -> Doc

valueprivateAccessInserted :: Access

valuerawNameToString :: RawName -> String

valuerelevant :: Relevance

valuesameCohesion :: Cohesion -> Cohesion -> Bool

Equality ignoring origin.

valuesameErased :: Erased -> Erased -> Bool

Equality ignoring origin.

valuesameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool

Ignores Overlappable.

valuesameModality :: (LensModality a, LensModality b) => a -> b -> Bool

Equality ignoring origin.

valuesameName :: NamedName -> NamedName -> Bool

Equality of argument names of things modulo Range and Origin.

valuesamePolarity :: PolarityModality -> PolarityModality -> Bool

Equality for polarities.

valuesameQuantity :: Quantity -> Quantity -> Bool

Equality ignoring origin.

valuesameRelevance :: Relevance -> Relevance -> Bool

Equality ignoring origin.

valuesetCohesionMod :: LensModality a => LensSet a Cohesion

valuesetFreeVariablesArgInfo :: LensArgInfo a => LensSet a FreeVariables

valuesetHidingArgInfo :: LensArgInfo a => LensSet a Hiding

valuesetImportedName :: ImportedName' a a -> a -> ImportedName' a a

valuesetModalityArgInfo :: LensArgInfo a => LensSet a Modality

valuesetNameOf :: LensNamed a => Maybe (NameOf a) -> a -> a

valuesetNamedArg :: NamedArg a -> b -> NamedArg b

setNamedArg a b = updateNamedArg (const b) a

valuesetOriginArgInfo :: LensArgInfo a => LensSet a Origin

valuesetPolarityMod :: LensModality a => LensSet a PolarityModality

valuesetQuantityMod :: LensModality a => LensSet a Quantity

valuesetRelevanceMod :: LensModality a => LensSet a Relevance

valueshapeIrrelevant :: Relevance

valueshapeIrrelevantToIrrelevant :: Relevance -> Relevance

valueshapeIrrelevantToRelevant :: Relevance -> Relevance

Applied when working on types (unless --experimental-irrelevance).

valuesplittablePolarity :: LensModalPolarity a => a -> Bool

splittablePolarity pol == False iff we cannot split on a variable of pol.

valuestringToArgName :: String -> ArgName

valuestringToRawName :: String -> RawName

valuetopCohesion :: Cohesion

Absorptive element under addition.

valuetopModality :: Modality

Absorptive element under addition.

valuetopPolarity :: PolarityModality

Absorptive element under addition.

valuetopQuantity :: Quantity

Absorptive element is ω.

valuetopRelevance :: Relevance

Absorptive element under addition.

valueunitCohesion :: Cohesion

Identity under composition

valueunitModality :: Modality

Identity under composition

valueunitPolarity :: PolarityModality

Identity under composition.

valueunitQuantity :: Quantity

Identity element under composition

valueunitRelevance :: Relevance

Identity element under composition

valueunknownFreeVariables :: FreeVariables

valueunnamed :: a -> Named name a

valueunnamedArg :: ArgInfo -> a -> NamedArg a

valueunranged :: a -> Ranged a

Thing with no range info.

valueupdateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b

The functor instance for NamedArg would be ambiguous, so we give it another name here.

valueupdateNamedArgA

:: Applicative f
=> a -> f b
-> NamedArg a
-> f (NamedArg b)

valueusableCohesion :: LensCohesion a => a -> Bool

usableCohesion rel == False iff we cannot use a variable of rel.

valueusableModality :: LensModality a => a -> Bool

valueusablePolarity :: LensModalPolarity a => a -> Bool

usablePolarity pol == False iff we cannot use a variable of pol.

valueusableQuantity :: LensQuantity a => a -> Bool

A thing of quantity 0 is unusable, all others are usable.

valueusableRelevance :: LensRelevance a => a -> Bool

usableRelevance rel == False iff we cannot use a variable of rel.

valueuserNamed :: Ranged ArgName -> a -> Named_ a

valuevisible :: LensHiding a => a -> Bool

NotHidden arguments are visible.

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.

valuewithNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a]

valuewithStandardLock :: ModalPolarity -> PolarityModality

valuezeroCohesion :: Cohesion

Cohesion forms a monoid under addition, and even a semiring.

valuezeroModality :: Modality

Identity under addition

valuezeroPolarity :: PolarityModality

ModalPolarity forms a monoid under addition, and even a semiring.

valuezeroQuantity :: Quantity

Identity element under addition

valuezeroRelevance :: Relevance

Relevance forms a monoid under addition, and even a semiring.

datadata Access

Access modifier.

Constructors

PrivateAccess KwRange Origin
Store the Origin of the private block that lead to this qualifier. This is needed for more faithful printing of declarations. KwRange is the range of the private keyword.
PublicAccess

Instances9Eq, Ord, Show, NFData, Pretty, HasRange, …

Eq AccessDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord AccessDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show AccessDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData AccessDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty AccessDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange AccessDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange AccessDefined in Agda-2.8.0.2 · Agda.Syntax.Common
MakePrivate AccessDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions
EmbPrj AccessDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Abstract · orphan

classclass AllAreOpaque a where

Methods

jointOpacity :: a -> JointOpacity

Instances4AllAreOpaque

AllAreOpaque IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
AllAreOpaque (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
AllAreOpaque a => AllAreOpaque (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
AllAreOpaque a => AllAreOpaque [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Common

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.

Instances11Eq, Ord, Show, Generic, NFData, Null, …

Eq AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensAnnotation AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj AnnotationDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep Annotation = D1 ('MetaData "Annotation" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "Annotation" 'PrefixI 'True) (S1 ('MetaSel ('Just "annLock") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lock)))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

classclass AnyIsAbstract a where

Is any element of a collection an AbstractDef.

Methods

anyIsAbstract :: a -> IsAbstract

Instances4AnyIsAbstract

AnyIsAbstract IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
AnyIsAbstract (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
AnyIsAbstract a => AnyIsAbstract (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
AnyIsAbstract a => AnyIsAbstract [a]Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata Arg e

Constructors

Arg
- argInfo :: ArgInfo
- unArg :: e

Instances134Functor, Foldable, Traversable, Decoration, IsPrefixOf, MapNamedArgPattern, …

Functor ArgDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Foldable ArgDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Traversable ArgDefined in Agda-2.8.0.2 · Agda.Syntax.Common
MapNamedArgPattern NAPDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
Decoration ArgDefined in Agda-2.8.0.2 · Agda.Syntax.Common
StripAllProjections ArgsDefined in Agda-2.8.0.2 · Agda.Termination.TermCheck
IsPrefixOf ArgsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Abstract
MapNamedArgPattern a (NamedArg (Pattern' a))Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
Modify the content of VarP, and the closest surrounding NamedArg.
Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.
PatternLike a b => PatternLike a (Arg b)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
Eq e => Eq (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord e => Ord (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Show e => Show (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData e => NFData (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty a => Pretty (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
IsProjP a => IsProjP (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
IsInstantiatedMeta a => IsInstantiatedMeta (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.MetaVars
HasRange a => HasRange (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Subst a => Subst (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
PrettyTCM (Arg Expr)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Arg Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Arg Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Arg String)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Arg Bool)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (NamedArg Expr)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (NamedArg Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Reify i => Reify (Arg i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Skip reification of implicit and irrelevant args if option is off.
ToConcrete (SplitPattern (NamedArg Pattern))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete (UserPattern (NamedArg Pattern))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Reduce t => Reduce (Arg t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Simplify t => Simplify (Arg t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Instantiate t => Instantiate (Arg t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Normalise t => Normalise (Arg t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Free t => Free (Arg t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy
LensQuantity (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ToAbstract c => ToAbstract (Arg c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
Hilite a => Hilite (Arg a)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
DeclaredNames a => DeclaredNames (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
IsWithP p => IsWithP (Arg p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pattern
LensHiding (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensOrigin (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
AllMetas a => AllMetas (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVars
Apply [NamedArg (Pattern' a)]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
Make sure we only drop variable patterns.
PiApplyM a => PiApplyM (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Telescope
SynEq a => SynEq (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SyntacticEquality
LensRelevance (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensSort a => LensSort (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
IsMeta a => IsMeta (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
TermLike a => TermLike (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
LensModalPolarity (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
BlankVars a => BlankVars (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
AnyRigid a => AnyRigid (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.MetaVars.Occurs
SubstExpr a => SubstExpr (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
KillRange a => KillRange (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange a => SetRange (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
APatternLike a => APatternLike (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
BoundAndUsed a => BoundAndUsed (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.UsedNames
ExprLike a => ExprLike (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
LensAnnotation (Arg t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensArgInfo (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensCohesion (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFreeVariables (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensLock (Arg t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModality (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensNamed a => LensNamed (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ExprLike a => ExprLike (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Generic
CPatternLike p => CPatternLike (Arg p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pattern
PatternVars (Arg (Pattern' a))Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
PatternVars (NamedArg (Pattern' a))Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
GetDefs a => GetDefs (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Defs
NamesIn a => NamesIn (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Names
CountPatternVars a => CountPatternVars (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
PatternVarModalities a => PatternVarModalities (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
EnsureNoLetStms a => EnsureNoLetStms (NamedArg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.Abstract
Binder a => Binder (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
ToAbstract r => ToAbstract (Arg r)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract
ToAbstract r => ToAbstract [Arg r]Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract
ExtractCalls a => ExtractCalls (Arg a)Defined in Agda-2.8.0.2 · Agda.Termination.TermCheck
StripAllProjections a => StripAllProjections (Arg a)Defined in Agda-2.8.0.2 · Agda.Termination.TermCheck
AbsTerm a => AbsTerm (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Abstract
EqualSy a => EqualSy (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Abstract
Ignores irrelevant arguments and modality. (And, of course, origin and free variables).
PrecomputeFreeVars a => PrecomputeFreeVars (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Precompute
NormaliseProjP a => NormaliseProjP (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Records
InstantiateFull t => InstantiateFull (Arg t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Match a => Match (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.DisplayForm
SubstWithOrigin (Arg Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.DisplayForm
SubstWithOrigin (Arg DisplayTerm)Defined in Agda-2.8.0.2 · Agda.TypeChecking.DisplayForm
ForcedVariables a => ForcedVariables (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Forcing
(Reduce a, ForceNotFree a) => ForceNotFree (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Reduce
UsableModality a => UsableModality (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Irrelevance
UsableRelevance a => UsableRelevance (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Irrelevance
NoProjectedVar a => NoProjectedVar (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.MetaVars
ReduceAndEtaContract a => ReduceAndEtaContract (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.MetaVars
MentionsMeta t => MentionsMeta (Arg t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.MetaVars.Mention
Occurs a => Occurs (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.MetaVars.Occurs
HasPolarity a => HasPolarity (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Polarity
ComputeOccurrences a => ComputeOccurrences (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Positivity
AllHoles p => AllHoles (Arg p)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Confluence
MetasToVars a => MetasToVars (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Confluence
ParallelReduce a => ParallelReduce (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Confluence
GetMatchables a => GetMatchables (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinPattern
IsFlexiblePattern a => IsFlexiblePattern (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS
EmbPrj a => EmbPrj (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
IApplyVars p => IApplyVars (NamedArg p)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Telescope.Path
Unquote a => Unquote (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
PatternToExpr p e => PatternToExpr (Arg p) (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
LabelPatVars a b => LabelPatVars (Arg a) (Arg b)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
TermToPattern a b => TermToPattern (Arg a) (Arg b)Defined in Agda-2.8.0.2 · Agda.Termination.TermCheck
TermToPattern a b => TermToPattern (Arg a) (Arg b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.Internal
Match a b => Match (Arg a) (Arg b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinMatch
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause
NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinPattern
PatternFrom a b => PatternFrom (Arg a) (Arg b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinPattern
AddContext (List1 (Arg Name), Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext (List1 (NamedArg Name), Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext ([Arg Name], Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext ([NamedArg Name], Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
type SubstArg (Arg a) = SubstArg aDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
type ConOfAbs (Arg a) = Arg (ConOfAbs a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ConOfAbs (SplitPattern (NamedArg Pattern)) = NamedArg PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ConOfAbs (UserPattern (NamedArg Pattern)) = NamedArg PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ReifiesTo (Arg i) = Arg (ReifiesTo i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
type AbsOfCon (Arg c) = Arg (AbsOfCon c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
type ADotT (Arg a) = ADotT aDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
type NameOf (Arg a) = NameOf aDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type PatternVarOut (Arg (Pattern' a)) = aDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
type PatternVarOut (NamedArg (Pattern' a)) = aDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
type TypeOf (Arg a) = Dom (TypeOf a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
type PatVarLabel (Arg b) = PatVarLabel bDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
type PatVar (Arg a) = PatVar aDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
type AbsOfRef (Arg r) = NamedArg (AbsOfRef r)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract
type AbsOfRef [Arg r] = [NamedArg (AbsOfRef r)]Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract

datadata ArgInfo

A function argument can be hidden and/or irrelevant.

Constructors

ArgInfo
- argInfoHiding :: Hiding
- argInfoModality :: Modality
- argInfoOrigin :: Origin
- argInfoFreeVariables :: FreeVariables
- argInfoAnnotation :: Annotation
  Sometimes we want a different kind of binder/pi-type, without it supporting any of the Modality interface.

Instances25Eq, Ord, Show, NFData, Null, HasRange, …

Eq ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensQuantity ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Hilite ArgInfoDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
LensHiding ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensOrigin ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SynEq ArgInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.SyntacticEquality
LensRelevance ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModalPolarity ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensAnnotation ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensArgInfo ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensCohesion ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFreeVariables ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensLock ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModality ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EqualSy ArgInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Abstract
Ignore origin and free variables.
ToTerm ArgInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
ChooseFlex ArgInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
EmbPrj ArgInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Unquote ArgInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote

typetype ArgName = String

Names in binders and arguments.

typetype Arity = Nat

datadata Associativity

Associativity.

NonAssoc LeftAssoc RightAssoc

Instances6Eq, Ord, Show, Pretty, ToTerm, EmbPrj

Eq AssociativityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord AssociativityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show AssociativityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty AssociativityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
ToTerm AssociativityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
EmbPrj AssociativityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

typetype BackendName = Text

datadata BinderNameOrigin

UserBinderName InsertedBinderName

Instances6Eq, Show, Generic, NFData, KillRange, Rep

Eq BinderNameOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show BinderNameOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic BinderNameOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData BinderNameOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange BinderNameOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep BinderNameOrigin = D1 ('MetaData "BinderNameOrigin" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "UserBinderName" 'PrefixI 'False) U1 :+: C1 ('MetaCons "InsertedBinderName" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

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

Eq BoundVariablePositionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord BoundVariablePositionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show BoundVariablePositionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData BoundVariablePositionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj BoundVariablePositionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata Catchall

Range of the CATCHALL pragma for a clause, if any. Nothing means no such pragma.

Constructors

YesCatchall Range
NoCatchall

Instances10Eq, Show, Generic, Semigroup, Monoid, NFData, …

Eq CatchallDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show CatchallDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic CatchallDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup CatchallDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Composition is left-biased, taking the left Range if both have one.
Monoid CatchallDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData CatchallDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null CatchallDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange CatchallDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj CatchallDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep Catchall = D1 ('MetaData "Catchall" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "YesCatchall" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "NoCatchall" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

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.

Instances26Bounded, Enum, Eq, Ord, Show, Generic, …

Bounded CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Order is given by implication: flatter is smaller.
Show CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty CohesionDefined 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.
HasRange CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Verbalize CohesionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors
KillRange CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensCohesion CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PartialOrd CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Flatter is smaller.
EmbPrj CohesionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Semigroup (UnderAddition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Cohesion forms a semigroup under addition.
Semigroup (UnderComposition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Cohesion forms a semigroup under composition.
Monoid (UnderAddition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Squash is the additive unit.
Monoid (UnderComposition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Continous is the multiplicative unit.
LeftClosedPOMonoid (UnderComposition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderAddition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderComposition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderAddition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderComposition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep Cohesion = D1 ('MetaData "Cohesion" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "Flat" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "Continuous" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Squash" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

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, …

Bounded ConOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum ConOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq ConOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord ConOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show ConOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic ConOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData ConOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ConOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj ConOriginDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep ConOrigin = D1 ('MetaData "ConOrigin" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) ((C1 ('MetaCons "ConOSystem" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ConOCon" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "ConORec" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ConOSplit" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

newtypenewtype Constr a

Constructors

Constr a

Instances2ToConcrete, ConOfAbs

ToConcrete (Constr Constructor)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ConOfAbs (Constr Constructor) = DeclarationDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete

datadata ConstructorOrPatternSynonym

Distinguish constructors from pattern synonyms.

IsConstructor IsPatternSynonym

Instances8Bounded, Enum, Show, Generic, NFData, Pretty, …

Bounded ConstructorOrPatternSynonymDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum ConstructorOrPatternSynonymDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show ConstructorOrPatternSynonymDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic ConstructorOrPatternSynonymDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData ConstructorOrPatternSynonymDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty ConstructorOrPatternSynonymDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj ConstructorOrPatternSynonymDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep ConstructorOrPatternSynonym = D1 ('MetaData "ConstructorOrPatternSynonym" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "IsConstructor" 'PrefixI 'False) U1 :+: C1 ('MetaCons "IsPatternSynonym" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

classclass CopatternMatchingAllowed a where

Can we construct a record by copattern matching?

Methods

copatternMatchingAllowed :: a -> Bool

Instances5CopatternMatchingAllowed

CopatternMatchingAllowed HasEtaDefined in Agda-2.8.0.2 · Agda.Syntax.Common
CopatternMatchingAllowed PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
CopatternMatchingAllowed ConHeadDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
CopatternMatchingAllowed DataOrRecordDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
CopatternMatchingAllowed EtaEqualityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base

datadata CoverageCheck

Coverage check? (Default is yes).

YesCoverageCheck NoCoverageCheck

Instances11Bounded, Enum, Eq, Ord, Show, Generic, …

Bounded CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange CoverageCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep CoverageCheck = D1 ('MetaData "CoverageCheck" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "YesCoverageCheck" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoCoverageCheck" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata Cubical

Variants of Cubical Agda.

CErased CFull

Instances6Eq, Show, Generic, NFData, EmbPrj, Rep

Eq CubicalDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show CubicalDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic CubicalDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData CubicalDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj CubicalDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep Cubical = D1 ('MetaData "Cubical" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "CErased" 'PrefixI 'False) U1 :+: C1 ('MetaCons "CFull" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata DisplayLHS

Distinguish parsing a DISPLAY pragma from an ordinary left hand side.

YesDisplayLHS NoDisplayLHS

Instances8Bounded, Enum, Eq, Show, Generic, Boolean, …

Bounded DisplayLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum DisplayLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq DisplayLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show DisplayLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic DisplayLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Boolean DisplayLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Common
IsBool DisplayLHSDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep DisplayLHS = D1 ('MetaData "DisplayLHS" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "YesDisplayLHS" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoDisplayLHS" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata Erased

A special case of Quantity: erased or not.

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

Instances12Eq, Ord, Show, Generic, NFData, Pretty, …

Eq ErasedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord ErasedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show ErasedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic ErasedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData ErasedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty ErasedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange ErasedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PrettyTCM ErasedDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Hilite ErasedDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
Erasure attributes are highlighted as symbols.
KillRange ErasedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup (UnderComposition Erased)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep Erased = D1 ('MetaData "Erased" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "Erased" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q0Origin)) :+: C1 ('MetaCons "NotErased" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QωOrigin)))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata ExpandedEllipsis

Constructors

ExpandedEllipsis
- ellipsisRange :: Range
- ellipsisWithArgs :: Int
NoEllipsis

Instances8Eq, Show, Semigroup, Monoid, NFData, Null, …

Eq ExpandedEllipsisDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show ExpandedEllipsisDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup ExpandedEllipsisDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid ExpandedEllipsisDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData ExpandedEllipsisDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null ExpandedEllipsisDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ExpandedEllipsisDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj ExpandedEllipsisDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata ExprKind

Expression kinds: Expressions or patterns.

IsExpr IsPattern

Instances2Eq, Show

Eq ExprKindDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show ExprKindDefined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata FileType

AgdaFileType MdFileType RstFileType TexFileType OrgFileType TypstFileType TreeFileType

Instances8Eq, Ord, Show, Generic, NFData, Pretty, …

Eq FileTypeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord FileTypeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show FileTypeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic FileTypeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData FileTypeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty FileTypeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj FileTypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep FileType = D1 ('MetaData "FileType" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) ((C1 ('MetaCons "AgdaFileType" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "MdFileType" 'PrefixI 'False) U1 :+: C1 ('MetaCons "RstFileType" 'PrefixI 'False) U1)) :+: ((C1 ('MetaCons "TexFileType" 'PrefixI 'False) U1 :+: C1 ('MetaCons "OrgFileType" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "TypstFileType" 'PrefixI 'False) U1 :+: C1 ('MetaCons "TreeFileType" 'PrefixI 'False) U1)))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata Fixity

Fixity of operators.

Constructors

Fixity
- fixityRange :: Range
  Range of the whole fixity declaration.
- fixityLevel :: !FixityLevel
- fixityAssoc :: !Associativity

Instances11Eq, Ord, Show, NFData, Pretty, Null, …

Eq FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFixity FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
ToTerm FixityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
EmbPrj FixityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata Fixity'

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

Constructors

Fixity'
- theFixity :: !Fixity
- theNotation :: Notation
- theNameRange :: Range
  Range of the name in the fixity declaration (used for correct highlighting, see issue #2140).

Instances12Eq, Show, NFData, Pretty, Null, KillRange, …

Eq Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Show Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pretty · orphan
Null Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFixity' Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFixity Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
PrimTerm Fixity'Defined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
PrimType Fixity'Defined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
ToTerm Fixity'Defined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
EmbPrj Fixity'Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata FixityLevel

Constructors

Unrelated
No fixity declared.
Related !PrecedenceLevel
Fixity level declared as the number.

Instances8Eq, Ord, Show, NFData, Pretty, Null, …

Eq FixityLevelDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord FixityLevelDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show FixityLevelDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData FixityLevelDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty FixityLevelDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null FixityLevelDefined in Agda-2.8.0.2 · Agda.Syntax.Common
ToTerm FixityLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
EmbPrj FixityLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata FreeVariables

Constructors

UnknownFVs
KnownFVs IntSet

Instances9Eq, Ord, Show, Semigroup, Monoid, NFData, …

Eq FreeVariablesDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord FreeVariablesDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show FreeVariablesDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup FreeVariablesDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid FreeVariablesDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData FreeVariablesDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange FreeVariablesDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFreeVariables FreeVariablesDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj FreeVariablesDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

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 HasEta' a

Does a record come with eta-equality?

Constructors

YesEta
NoEta a

Instances12Functor, Foldable, Traversable, CopatternMatchingAllowed, PatternMatchingAllowed, Eq, …

Functor HasEta'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Foldable HasEta'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Traversable HasEta'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
CopatternMatchingAllowed HasEtaDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PatternMatchingAllowed HasEtaDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq a => Eq (HasEta' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord a => Ord (HasEta' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Show a => Show (HasEta' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData a => NFData (HasEta' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange a => HasRange (HasEta' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange a => KillRange (HasEta' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj a => EmbPrj (HasEta' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

typetype HasEta0 = HasEta' ()

classclass HasOverlapMode a where

Methods

lensOverlapMode :: Lens' a OverlapMode

Instances2HasOverlapMode

HasOverlapMode OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasOverlapMode CandidateDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base

datadata Hiding

Constructors

Hidden
Instance Overlappable
NotHidden

Instances15Eq, Ord, Show, Semigroup, Monoid, NFData, …

Eq HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Hiding is an idempotent partial monoid, with unit NotHidden. Instance and NotHidden are incompatible.
Monoid HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Verbalize HidingDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors
LensHiding HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
ChooseFlex HidingDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
EmbPrj HidingDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Unquote HidingDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote

typetype HidingDirective' n m = [ImportedName' n m]

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

ImportDirective
- importDirRange :: Range
- using :: Using' n m
- hiding :: HidingDirective' n m
- impRenaming :: RenamingDirective' n m
- publicOpen :: Maybe KwRange
  Only for open. Exports the opened names from the current module. Range of the public keyword.

Instances10Eq, Show, Semigroup, Monoid, NFData, Pretty, …

(Eq m, Eq n) => Eq (ImportDirective' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Show m, Show n) => Show (ImportDirective' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange n, HasRange m) => Semigroup (ImportDirective' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange n, HasRange m) => Monoid (ImportDirective' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(NFData a, NFData b) => NFData (ImportDirective' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ranges are not forced.
(Pretty a, Pretty b) => Pretty (ImportDirective' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
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).
(HasRange a, HasRange b) => HasRange (ImportDirective' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Hilite m, Hilite n, Hilite (RenamingTo m), Hilite (RenamingTo n)) => Hilite (ImportDirective' m n)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
(KillRange a, KillRange b) => KillRange (ImportDirective' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata ImportedName' n m

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

Constructors

ImportedModule m
Imported module name of type m.
ImportedName n
Imported name of type n.

Instances11PrettyTCM, Eq, Ord, Show, NFData, Pretty, …

PrettyTCM ImportedNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
(Hilite (RenamingTo m), Hilite (RenamingTo n)) => Hilite (RenamingTo (ImportedName' m n))Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
(Eq m, Eq n) => Eq (ImportedName' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Ord m, Ord n) => Ord (ImportedName' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Show m, Show n) => Show (ImportedName' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(NFData a, NFData b) => NFData (ImportedName' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Pretty a, Pretty b) => Pretty (ImportedName' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange a, HasRange b) => HasRange (ImportedName' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Hilite m, Hilite n) => Hilite (ImportedName' m n)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
(KillRange a, KillRange b) => KillRange (ImportedName' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

newtypenewtype InteractionId

Constructors

InteractionId
- interactionId :: Nat

Instances18Enum, Eq, Integral, Num, Ord, Read, …

Enum InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Integral InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Num InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Read InteractionIdDefined in Agda-2.8.0.2 · Agda.Interaction.Base · orphan
Real InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData InteractionPointsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
ToJSON InteractionIdDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
Pretty InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasFresh InteractionIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
PrettyTCM InteractionIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
ToConcrete InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
EncodeTCM InteractionIdDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
KillRange InteractionIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type ConOfAbs InteractionId = ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete

datadata IsAbstract

Abstract or concrete.

AbstractDef ConcreteDef

Instances15Eq, Ord, Show, Generic, Semigroup, Monoid, …

Eq IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup computes if any of several is an AbstractDef.
Monoid IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Default is ConcreteDef.
NFData IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
AnyIsAbstract IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensIsAbstract IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Boolean IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
IsBool IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
MakeAbstract IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Definitions
EmbPrj IsAbstractDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep IsAbstract = D1 ('MetaData "IsAbstract" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "AbstractDef" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ConcreteDef" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata IsInfix

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

InfixDef PrefixDef

Instances3Eq, Ord, Show

Eq IsInfixDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord IsInfixDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show IsInfixDefined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata IsInstance

Is this definition eligible for instance search?

Constructors

InstanceDef KwRange
Range of the instance keyword.
NotInstanceDef

Instances7Eq, Ord, Show, NFData, HasRange, KillRange, …

Eq IsInstanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord IsInstanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show IsInstanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData IsInstanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange IsInstanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange IsInstanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj IsInstanceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata IsMacro

Is this a macro definition?

MacroDef NotMacroDef

Instances8Eq, Ord, Show, Generic, NFData, HasRange, …

Eq IsMacroDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord IsMacroDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show IsMacroDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic IsMacroDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData IsMacroDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange IsMacroDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange IsMacroDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep IsMacro = D1 ('MetaData "IsMacro" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "MacroDef" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NotMacroDef" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata IsMain

IsMain NotMain

Instances4Eq, Show, Semigroup, Monoid

Eq IsMainDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show IsMainDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup IsMainDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Conjunctive semigroup (NotMain is absorbing).
Monoid IsMainDefined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata IsOpaque

Opaque or transparent.

Constructors

OpaqueDef !OpaqueId
This definition is opaque, and it is guarded by the given opaque block.
TransparentDef

Instances10Eq, Ord, Show, Generic, NFData, KillRange, …

Eq IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
AllAreOpaque IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensIsOpaque IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj IsOpaqueDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep IsOpaque = D1 ('MetaData "IsOpaque" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "OpaqueDef" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'SourceUnpack 'SourceStrict 'DecidedUnpack) (Rec0 OpaqueId)) :+: C1 ('MetaCons "TransparentDef" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata JointOpacity

Monoid representing the combined opaque blocks of a Foldable containing possibly-opaque declarations.

Constructors

UniqueOpaque !OpaqueId
Every definition agrees on what opaque block they belong to.
DifferentOpaque !(HashSet OpaqueId)
More than one opaque block was found.
NoOpaque
Nothing here is opaque.

Instances2Semigroup, Monoid

Semigroup JointOpacityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid JointOpacityDefined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata Language

Agda variants.

Only some variants are tracked.

Constructors

WithoutK
WithK
Cubical Cubical

Instances7Eq, Show, Generic, NFData, KillRange, EmbPrj, …

Eq LanguageDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show LanguageDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic LanguageDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData LanguageDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange LanguageDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj LanguageDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep Language = D1 ('MetaData "Language" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "WithoutK" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "WithK" 'PrefixI 'False) U1 :+: C1 ('MetaCons "Cubical" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cubical))))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

classclass LensAnnotation a where

Methods

getAnnotation :: a -> Annotation
setAnnotation :: Annotation -> a -> a
mapAnnotation :: (Annotation -> Annotation) -> a -> a

Instances4LensAnnotation

LensAnnotation AnnotationDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensAnnotation ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensAnnotation (Arg t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensAnnotation (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal

classclass LensArgInfo a where

Methods

getArgInfo :: a -> ArgInfo
setArgInfo :: ArgInfo -> a -> a
mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a

Instances6LensArgInfo

LensArgInfo ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensArgInfo DefinitionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensArgInfo ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
LensArgInfo (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensArgInfo (FlexibleVar a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
LensArgInfo (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal

classclass LensCohesion a where

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

Methods

getCohesion :: a -> Cohesion
setCohesion :: Cohesion -> a -> a
mapCohesion :: (Cohesion -> Cohesion) -> a -> a

Instances6LensCohesion

LensCohesion ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensCohesion CohesionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensCohesion ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensCohesion ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
LensCohesion (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensCohesion (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal

classclass LensFixity a where

Methods

lensFixity :: Lens' a Fixity

Instances7LensFixity, …

LensFixity NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensFixity QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensFixity FixityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFixity Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFixity NewNotationDefined in Agda-2.8.0.2 · Agda.Syntax.Notation
LensFixity AbstractNameDefined in Agda-2.8.0.2 · Agda.Syntax.Scope.Base
LensFixity (ThingWithFixity a)Defined in Agda-2.8.0.2 · Agda.Syntax.Fixity

classclass LensFixity' a where

Methods

lensFixity' :: Lens' a Fixity'

Instances4LensFixity'

LensFixity' NameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensFixity' QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
LensFixity' Fixity'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFixity' (ThingWithFixity a)Defined in Agda-2.8.0.2 · Agda.Syntax.Fixity

classclass LensFreeVariables a where

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

Methods

getFreeVariables :: a -> FreeVariables
setFreeVariables :: FreeVariables -> a -> a
mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a

Instances4LensFreeVariables

LensFreeVariables ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFreeVariables FreeVariablesDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFreeVariables (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensFreeVariables (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal

classclass LensHiding a where

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

Methods

getHiding :: a -> Hiding
setHiding :: Hiding -> a -> a
mapHiding :: (Hiding -> Hiding) -> a -> a

Instances12LensHiding, …

LensHiding LamBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
LensHiding TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
LensHiding ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensHiding HidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensHiding LamBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
LensHiding TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
LensHiding ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
LensHiding (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensHiding (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensHiding (FlexibleVar a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
LensHiding (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
LensHiding a => LensHiding (Named nm a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

classclass LensIsAbstract a where

Methods

lensIsAbstract :: Lens' a IsAbstract

Instances5LensIsAbstract

LensIsAbstract IsAbstractDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensIsAbstract MetaInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensIsAbstract TCEnvDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensIsAbstract (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info
LensIsAbstract (Closure a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base

classclass LensIsOpaque a where

Methods

lensIsOpaque :: Lens' a IsOpaque

Instances3LensIsOpaque

LensIsOpaque IsOpaqueDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensIsOpaque TCEnvDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensIsOpaque (DefInfo' t)Defined in Agda-2.8.0.2 · Agda.Syntax.Info

classclass LensLock a where

Methods

getLock :: a -> Lock
setLock :: Lock -> a -> a
mapLock :: (Lock -> Lock) -> a -> a

Instances4LensLock

LensLock ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensLock LockDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensLock (Arg t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensLock (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal

classclass LensModalPolarity a where

A lens to access the PolarityModality attribute in data structures. Minimal implementation: getModalPolarity and mapModalPolarity or LensModality.

Methods

getModalPolarity :: a -> PolarityModality
setModalPolarity :: PolarityModality -> a -> a
mapModalPolarity :: (PolarityModality -> PolarityModality) -> a -> a

Instances9LensModalPolarity, …

LensModalPolarity ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModalPolarity ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModalPolarity PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModalPolarity DefinitionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensModalPolarity MetaInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensModalPolarity RemoteMetaVariableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensModalPolarity ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
LensModalPolarity (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModalPolarity (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal

classclass LensModality a where

Methods

getModality :: a -> Modality
setModality :: Modality -> a -> a
mapModality :: (Modality -> Modality) -> a -> a

Instances12LensModality, …

LensModality ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModality ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModality DefinitionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensModality MetaInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensModality MetaVariableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensModality RemoteMetaVariableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensModality ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
LensModality (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModality (VarOcc' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy
LensModality (FlexibleVar a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
LensModality (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
LensModality (FreeEnv' a b c)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy

classclass LensNamed a where

Accessor/editor for the nameOf component.

Associated types

type family NameOf a
The type of the name

Methods

lensNamed :: Lens' a (Maybe (NameOf a))

Instances4LensNamed

LensNamed (Maybe a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensNamed a => LensNamed (Arg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensNamed (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensNamed (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal

classclass LensOrigin a where

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

Methods

getOrigin :: a -> Origin
setOrigin :: Origin -> a -> a
mapOrigin :: (Origin -> Origin) -> a -> a

Instances9LensOrigin, …

LensOrigin ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensOrigin OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensOrigin AppInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Info
LensOrigin ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
LensOrigin (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensOrigin (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensOrigin (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Elim
This instance cheats on Proj, use with care. Projs are always assumed to be UserWritten, since they have no ArgInfo. Same for IApply
LensOrigin (FlexibleVar a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
LensOrigin (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal

classclass LensQuantity a where

Methods

getQuantity :: a -> Quantity
setQuantity :: Quantity -> a -> a
mapQuantity :: (Quantity -> Quantity) -> a -> a

Instances12LensQuantity, …

LensQuantity ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensQuantity ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensQuantity QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensQuantity DefinitionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensQuantity MetaInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensQuantity MetaVariableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensQuantity RemoteMetaVariableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensQuantity ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
LensQuantity (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensQuantity (VarOcc' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy
LensQuantity (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
LensQuantity (FreeEnv' a b c)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy

classclass LensRelevance a where

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

Methods

getRelevance :: a -> Relevance
setRelevance :: Relevance -> a -> a
mapRelevance :: (Relevance -> Relevance) -> a -> a

Instances13LensRelevance, …

LensRelevance ArgInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensRelevance ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensRelevance RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensRelevance TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete
LensRelevance DefinitionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensRelevance MetaInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensRelevance MetaVariableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensRelevance RemoteMetaVariableDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
LensRelevance ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types
LensRelevance (Arg e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LensRelevance (VarOcc' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy
LensRelevance (Dom' t e)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
LensRelevance (FreeEnv' a b c)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy

datadata Lock

Constructors

IsNotLock
IsLock LockOrigin
In the future there might be different kinds of them. For now we assume lock weakening.

Instances10Eq, Ord, Show, Generic, NFData, Pretty, …

Eq LockDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord LockDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show LockDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic LockDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData LockDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty LockDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null LockDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensLock LockDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj LockDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep Lock = D1 ('MetaData "Lock" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "IsNotLock" 'PrefixI 'False) U1 :+: C1 ('MetaCons "IsLock" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LockOrigin)))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata LockOrigin

Constructors

LockOLock
The user wrote @lock.
LockOTick
The user wrote @tick.

Instances7Bounded, Enum, Eq, Ord, Show, Generic, …

Bounded LockOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum LockOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq LockOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord LockOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show LockOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic LockOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep LockOrigin = D1 ('MetaData "LockOrigin" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "LockOLock" 'PrefixI 'False) U1 :+: C1 ('MetaCons "LockOTick" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata MaybePlaceholder e

Placeholders are used to represent the underscores in a section.

Constructors

Placeholder !PositionInName
NoPlaceholder !(Maybe PositionInName) e
The second argument is used only (but not always) for name parts other than underscores.

Instances11Functor, Foldable, Traversable, Eq, Ord, Show, …

Functor MaybePlaceholderDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Foldable MaybePlaceholderDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Traversable MaybePlaceholderDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq e => Eq (MaybePlaceholder e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord e => Ord (MaybePlaceholder e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Show e => Show (MaybePlaceholder e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData a => NFData (MaybePlaceholder a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty a => Pretty (MaybePlaceholder a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pretty · orphan
HasRange a => HasRange (MaybePlaceholder a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange a => KillRange (MaybePlaceholder a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ExprLike a => ExprLike (MaybePlaceholder a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Generic

datadata MetaId

Meta-variable identifiers use the same structure as NameIds.

Constructors

MetaId
- metaId :: !Word64
- metaModule :: !ModuleNameHash

Instances28Enum, Eq, Ord, Show, Generic, NFData, …

Enum MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
The record selectors are not included in the resulting strings.
Generic MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Hashable MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
ToJSON MetaIdDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
Pretty MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasFresh MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
IsInstantiatedMeta MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.MetaVars
UnFreezeMeta MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.MetaVars
PrettyTCM MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Reify MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
EncodeTCM MetaIdDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
GetDefs MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Defs
NamesIn MetaIdDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Names
FromTerm MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
PrimTerm MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
PrimType MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
ToTerm MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive
EmbPrj MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Unquote MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Singleton MetaId MetaSetDefined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy
Singleton MetaId ()Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy · orphan
InstantiateFull (Judgement MetaId)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'SourceUnpack 'SourceStrict 'DecidedUnpack) (Rec0 Word64) :*: S1 ('MetaSel ('Just "metaModule") 'SourceUnpack 'SourceStrict 'DecidedUnpack) (Rec0 ModuleNameHash)))Defined in Agda-2.8.0.2 · Agda.Syntax.Common
type ReifiesTo MetaId = ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract

datadata ModalPolarity

The different polarity options

Constructors

UnusedPolarity
argument will not be used.
StrictlyPositive
argument will only be used in strictly positive position.
Positive
argument will only be used in positive position.
Negative
argument will only be used in negative position.
MixedPolarity
we don't know anything, argument can be used anywhere.

Instances12Bounded, Enum, Eq, Ord, Show, Generic, …

Bounded ModalPolarityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum ModalPolarityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq ModalPolarityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord ModalPolarityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show ModalPolarityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic ModalPolarityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty ModalPolarityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PrettyTCM ModalPolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Verbalize ModalPolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors
PartialOrd ModalPolarityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
The derived Ord instance for ModalPolarity is just used for serialisation and has no particular meaning. The actual order on modalities is a partial order.
EmbPrj ModalPolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep ModalPolarity = D1 ('MetaData "ModalPolarity" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) ((C1 ('MetaCons "UnusedPolarity" 'PrefixI 'False) U1 :+: C1 ('MetaCons "StrictlyPositive" 'PrefixI 'False) U1) :+: (C1 ('MetaCons "Positive" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "Negative" 'PrefixI 'False) U1 :+: C1 ('MetaCons "MixedPolarity" 'PrefixI 'False) U1)))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

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.
- modPolarity :: PolarityModality
  Polarity annotations (strictly positive, ...)

Instances32Eq, Ord, Show, Generic, NFData, Pretty, …

Eq ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PrettyTCM ModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Verbalize ModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors
LensQuantity ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Hilite ModalityDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
LensRelevance ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModalPolarity ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensCohesion ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensModality ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PartialOrd ModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Dominance ordering.
EmbPrj ModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Unquote ModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
IsVarSet () AllowedVarDefined in Agda-2.8.0.2 · Agda.TypeChecking.MetaVars.Occurs · orphan
Semigroup (UnderAddition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pointwise addition.
Semigroup (UnderComposition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pointwise composition.
Monoid (UnderAddition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pointwise additive unit.
Monoid (UnderComposition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pointwise composition unit.
LeftClosedPOMonoid (UnderComposition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderAddition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderComposition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderAddition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderComposition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Singleton (Nat, Modality) ForcedVariableCollectionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Forcing
type Rep Modality = D1 ('MetaData "Modality" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "Modality" 'PrefixI 'True) ((S1 ('MetaSel ('Just "modRelevance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Relevance) :*: S1 ('MetaSel ('Just "modQuantity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Quantity)) :*: (S1 ('MetaSel ('Just "modCohesion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cohesion) :*: S1 ('MetaSel ('Just "modPolarity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PolarityModality))))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata NameId

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

Constructors

NameId !Word64 !ModuleNameHash

Instances14Enum, Eq, Ord, Show, Generic, NFData, …

Enum NameIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq NameIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord NameIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show NameIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic NameIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData NameIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Hashable NameIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty NameIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasFresh NameIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange NameIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj NameIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
MonadFresh NameId m => MonadFresh NameId (AbsToConT m)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Monad m => MonadFresh NameId (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure
type Rep NameId = D1 ('MetaData "NameId" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "NameId" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'SourceUnpack 'SourceStrict 'DecidedUnpack) (Rec0 Word64) :*: S1 ('MetaSel 'Nothing 'SourceUnpack 'SourceStrict 'DecidedUnpack) (Rec0 ModuleNameHash)))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

familytype family NameOf a

The type of the name

Instances4NameOf

type NameOf (Arg a) = NameOf aDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type NameOf (Named name a) = nameDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type NameOf (Dom' t e) = NamedNameDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
type NameOf (Maybe a) = aDefined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata Named name a

Something potentially carrying a name.

Constructors

Named
- nameOf :: Maybe name
- namedThing :: a

Instances76MapNamedArgPattern, PatternLike, Functor, Foldable, Traversable, Pretty, …

MapNamedArgPattern NAPDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
MapNamedArgPattern a (NamedArg (Pattern' a))Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
Modify the content of VarP, and the closest surrounding NamedArg.
Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.
PatternLike a b => PatternLike a (Named x b)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
Functor (Named name)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Foldable (Named name)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Traversable (Named name)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty e => Pretty (Named_ e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
DeBruijn a => DeBruijn (Named_ a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute.DeBruijn
PrettyTCM (NamedArg Expr)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (NamedArg Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Named_ Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
ToConcrete (SplitPattern (NamedArg Pattern))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete (UserPattern (NamedArg Pattern))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Apply [NamedArg (Pattern' a)]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
Make sure we only drop variable patterns.
Decoration (Named name)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
PatternVars (NamedArg (Pattern' a))Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
EnsureNoLetStms a => EnsureNoLetStms (NamedArg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
EnsureNoLetStms a => EnsureNoLetStms (Named_ a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
NormaliseProjP a => NormaliseProjP (Named_ a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Records
IApplyVars p => IApplyVars (NamedArg p)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Telescope.Path
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause
(Eq name, Eq a) => Eq (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Ord name, Ord a) => Ord (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Show name, Show a) => Show (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(NFData name, NFData a) => NFData (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
IsProjP a => IsProjP (Named n a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Name
AddContext (List1 (NamedArg Name), Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext ([NamedArg Name], Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
HasRange a => HasRange (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Subst a => Subst (Named name a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
Reify i => Reify (Named n i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
ToConcrete a => ToConcrete (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Simplify t => Simplify (Named name t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Normalise t => Normalise (Named name t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Free t => Free (Named nm t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy
ToAbstract c => ToAbstract (Named name c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
(Hilite a, HasRange n) => Hilite (Named n a)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
DeclaredNames a => DeclaredNames (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
IsWithP p => IsWithP (Named n p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pattern
LensHiding a => LensHiding (Named nm a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
PiApplyM a => PiApplyM (Named n a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Telescope
BlankVars a => BlankVars (Named s a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
SubstExpr a => SubstExpr (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
(KillRange name, KillRange a) => KillRange (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange a => SetRange (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
APatternLike a => APatternLike (Named n a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
BoundAndUsed a => BoundAndUsed (Named n a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.UsedNames
ExprLike a => ExprLike (Named x a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
LensNamed (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ExprLike a => ExprLike (Named name a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Generic
CPatternLike p => CPatternLike (Named n p)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pattern
NamesIn a => NamesIn (Named n a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Names
CountPatternVars a => CountPatternVars (Named x a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
PatternVarModalities a => PatternVarModalities (Named s a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.Abstract
Binder a => Binder (Named x a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
ToAbstract r => ToAbstract (Named name r)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract
InstantiateFull t => InstantiateFull (Named name t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
IsFlexiblePattern a => IsFlexiblePattern (Named name a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
PatternToExpr p e => PatternToExpr (Named n p) (Named n e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
LabelPatVars a b => LabelPatVars (Named x a) (Named x b)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
TermToPattern a b => TermToPattern (Named c a) (Named c b)Defined in Agda-2.8.0.2 · Agda.Termination.TermCheck
TermToPattern a b => TermToPattern (Named c a) (Named c b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Patterns.Internal
type SubstArg (Named name a) = SubstArg aDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
type ConOfAbs (Named name a) = Named name (ConOfAbs a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ConOfAbs (SplitPattern (NamedArg Pattern)) = NamedArg PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ConOfAbs (UserPattern (NamedArg Pattern)) = NamedArg PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ReifiesTo (Named n i) = Named n (ReifiesTo i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
type AbsOfCon (Named name c) = Named name (AbsOfCon c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
type ADotT (Named n a) = ADotT aDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
type NameOf (Named name a) = nameDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type PatternVarOut (NamedArg (Pattern' a)) = aDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
type PatVarLabel (Named x b) = PatVarLabel bDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
type PatVar (Named s a) = PatVar aDefined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
type AbsOfRef (Named name r) = Named name (AbsOfRef r)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ReflectedToAbstract

typetype NamedArg a = Arg (Named_ a)

Only Hidden arguments can have names.

typetype NamedName = WithOrigin (Ranged ArgName)

Standard argument names.

typetype Named_ = Named NamedName

Standard naming.

typetype Nat = Int

Number >= 0.

typetype Nat1 = Nat

Number >= 1.

typetype Notation = [NotationPart]

Notation as provided by the syntax declaration.

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, …

Eq NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Pretty · orphan
HasRange NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange NotationPartDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj NotationPartDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata OpaqueId

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

Constructors

OpaqueId !Word64 !ModuleNameHash

Instances12Enum, Eq, Ord, Show, Generic, NFData, …

Enum OpaqueIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq OpaqueIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord OpaqueIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show OpaqueIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic OpaqueIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData OpaqueIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Hashable OpaqueIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty OpaqueIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasFresh OpaqueIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
KillRange OpaqueIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj OpaqueIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep OpaqueId = D1 ('MetaData "OpaqueId" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "OpaqueId" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'SourceUnpack 'SourceStrict 'DecidedUnpack) (Rec0 Word64) :*: S1 ('MetaSel 'Nothing 'SourceUnpack 'SourceStrict 'DecidedUnpack) (Rec0 ModuleNameHash)))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

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, LensOrigin, …

Eq OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
LensOrigin OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
ChooseFlex OriginDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.LHS.Problem
EmbPrj OriginDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata OriginIrrelevant

Origin of Irrelevant.

Constructors

OIrrInferred
User wrote nothing.
OIrrDot Range
User wrote ".".
OIrrIrr Range
User wrote "@irr".
OIrrIrrelevant Range
User wrote "@irrelevant".

Instances12Show, Generic, Semigroup, Monoid, NFData, Pretty, …

Show OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Right-biased composition, because the left relevance acts as context, and the right one as occurrence.
Monoid OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj OriginIrrelevantDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep OriginIrrelevant = D1 ('MetaData "OriginIrrelevant" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) ((C1 ('MetaCons "OIrrInferred" 'PrefixI 'False) U1 :+: C1 ('MetaCons "OIrrDot" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "OIrrIrr" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "OIrrIrrelevant" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata OriginRelevant

Origin of Relevant.

Constructors

ORelInferred
User wrote nothing.
ORelRelevant Range
User wrote "@relevant".

Instances12Show, Generic, Semigroup, Monoid, NFData, Pretty, …

Show OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange OriginRelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj OriginRelevantDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep OriginRelevant = D1 ('MetaData "OriginRelevant" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "ORelInferred" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ORelRelevant" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata OriginShapeIrrelevant

Origin of ShapeIrrelevant.

Constructors

OShIrrInferred
User wrote nothing.
OShIrrDotDot Range
User wrote "..".
OShIrrShIrr Range
User wrote "@shirr".
OShIrrShapeIrrelevant Range
User wrote "@shape-irrelevant".

Instances12Show, Generic, Semigroup, Monoid, NFData, Pretty, …

Show OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Right-biased composition, because the left relevance acts as context, and the right one as occurrence.
Monoid OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj OriginShapeIrrelevantDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep OriginShapeIrrelevant = D1 ('MetaData "OriginShapeIrrelevant" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) ((C1 ('MetaCons "OShIrrInferred" 'PrefixI 'False) U1 :+: C1 ('MetaCons "OShIrrDotDot" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "OShIrrShIrr" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "OShIrrShapeIrrelevant" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

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, …

Bounded OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasOverlapMode OverlapModeDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj OverlapModeDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

datadata Overlappable

YesOverlap NoOverlap

Instances6Eq, Ord, Show, Semigroup, Monoid, NFData

Eq OverlappableDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord OverlappableDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show OverlappableDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup OverlappableDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Just for the Hiding instance. Should never combine different overlapping.
Monoid OverlappableDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData OverlappableDefined in Agda-2.8.0.2 · Agda.Syntax.Common

classclass PatternMatchingAllowed a where

Can we pattern match on the record constructor?

Methods

patternMatchingAllowed :: a -> Bool

Instances5PatternMatchingAllowed

PatternMatchingAllowed HasEtaDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PatternMatchingAllowed PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PatternMatchingAllowed InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PatternMatchingAllowed DataOrRecordDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
PatternMatchingAllowed EtaEqualityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base

datadata PatternOrCopattern

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

Constructors

PatternMatching
Can match on the record constructor.
CopatternMatching
Can copattern match using the projections. (Default.)

Instances17Bounded, Enum, Eq, Ord, Show, NFData, …

Bounded PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange DataOrRecordDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
CopatternMatchingAllowed HasEtaDefined in Agda-2.8.0.2 · Agda.Syntax.Common
CopatternMatchingAllowed PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
CopatternMatchingAllowed DataOrRecordDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
PatternMatchingAllowed HasEtaDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PatternMatchingAllowed PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PatternMatchingAllowed DataOrRecordDefined in Agda-2.8.0.2 · Agda.Syntax.Internal
EmbPrj PatternOrCopatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
EmbPrj DataOrRecordDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Internal · orphan

datadata PolarityModality

Constructors

PolarityModality
- modPolarityAnn :: ModalPolarity
  The actual polarity of the variable
- modPolarityOrigin :: ModalPolarity
  The original polarity annotation by the user
- modPolarityLock :: ModalPolarity
  The locks of the variable (= composition of all denominators the variable has been left divided by)

Instances26Bounded, Eq, Ord, Show, Generic, NFData, …

Bounded PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PrettyTCM PolarityModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Verbalize PolarityModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors
LensModalPolarity PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PartialOrd PolarityModalityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj PolarityModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Semigroup (UnderAddition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ModalPolarity forms a semigroup under addition.
Semigroup (UnderComposition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ModalPolarity forms a semigroup under composition.
Monoid (UnderAddition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
'' is the additive unit.
Monoid (UnderComposition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Continous is the multiplicative unit.
LeftClosedPOMonoid (UnderComposition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderAddition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderComposition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderAddition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderComposition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep PolarityModality = D1 ('MetaData "PolarityModality" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "PolarityModality" 'PrefixI 'True) (S1 ('MetaSel ('Just "modPolarityAnn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModalPolarity) :*: (S1 ('MetaSel ('Just "modPolarityOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModalPolarity) :*: S1 ('MetaSel ('Just "modPolarityLock") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModalPolarity))))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

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

Eq PositionInNameDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord PositionInNameDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show PositionInNameDefined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata PositivityCheck

Positivity check? (Default = True).

YesPositivityCheck NoPositivityCheck

Instances11Bounded, Enum, Eq, Ord, Show, Generic, …

Bounded PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange PositivityCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep PositivityCheck = D1 ('MetaData "PositivityCheck" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "YesPositivityCheck" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoPositivityCheck" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

typetype PrecedenceLevel = Double

Precedence levels for operators.

newtypenewtype ProblemId

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

Constructors

ProblemId Nat

Instances15Enum, Eq, Integral, Num, Ord, Real, …

Enum ProblemIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq ProblemIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Integral ProblemIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Num ProblemIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord ProblemIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Real ProblemIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show ProblemIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData ProblemIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
ToJSON ProblemIdDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
Pretty ProblemIdDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasFresh ProblemIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base
PrettyTCM ProblemIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
EncodeTCM ProblemIdDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphan
EmbPrj ProblemIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Monad m => MonadFresh ProblemId (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure

datadata ProjOrigin

Where does a projection come from?

Constructors

ProjPrefix
User wrote a prefix projection.
ProjPostfix
User wrote a postfix projection.
ProjSystem
Projection was generated by the system.

Instances10Bounded, Enum, Eq, Ord, Show, Generic, …

Bounded ProjOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum ProjOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq ProjOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord ProjOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show ProjOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic ProjOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData ProjOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange ProjOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj ProjOriginDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep ProjOrigin = D1 ('MetaData "ProjOrigin" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "ProjPrefix" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "ProjPostfix" 'PrefixI 'False) U1 :+: C1 ('MetaCons "ProjSystem" 'PrefixI 'False) U1))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata Q0Origin

Origin of Quantity0.

Constructors

Q0Inferred
User wrote nothing.
Q0 Range
User wrote "@0".
Q0Erased Range
User wrote "@erased".

Instances14Eq, Ord, Show, Generic, Semigroup, Monoid, …

Eq Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Right-biased composition, because the left quantity acts as context, and the right one as occurrence.
Monoid Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange Q0OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj Q0OriginDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep Q0Origin = D1 ('MetaData "Q0Origin" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "Q0Inferred" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "Q0" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q0Erased" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata Q1Origin

Origin of Quantity1.

Constructors

Q1Inferred
User wrote nothing.
Q1 Range
User wrote "@1".
Q1Linear Range
User wrote "@linear".

Instances14Eq, Ord, Show, Generic, Semigroup, Monoid, …

Eq Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Right-biased composition, because the left quantity acts as context, and the right one as occurrence.
Monoid Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange Q1OriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj Q1OriginDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep Q1Origin = D1 ('MetaData "Q1Origin" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "Q1Inferred" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "Q1" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q1Linear" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

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

Quantity0 Q0Origin
Zero uses {0}, erased at runtime.
Quantity1 Q1Origin
Linear use {1} (could be updated destructively). Mostly TODO (needs postponable constraints between quantities to compute uses).
Quantityω QωOrigin
Unrestricted use ℕ.

Instances27Eq, Ord, Show, Generic, NFData, Pretty, …

Eq QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty QuantityDefined 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.
HasRange QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PrettyTCM QuantityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Verbalize QuantityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors
LensQuantity QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Hilite QuantityDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
If the Quantity attribute comes with a Range, highlight the corresponding attribute as Symbol.
KillRange QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PartialOrd QuantityDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Note that the order is ω ≤ 0,1, more options is smaller.
EmbPrj QuantityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Unquote QuantityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Semigroup (UnderAddition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup (UnderComposition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Composition of quantities (multiplication).
Quantity0 is dominant. Quantity1 is neutral.
Right-biased for origin.
Monoid (UnderAddition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid (UnderComposition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
In the absense of finite quantities besides 0, ω is the unit. Otherwise, 1 is the unit.
LeftClosedPOMonoid (UnderComposition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderAddition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderComposition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderAddition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderComposition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep Quantity = D1 ('MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "Quantity0" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q0Origin)) :+: (C1 ('MetaCons "Quantity1" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q1Origin)) :+: C1 ('MetaCons "Quantity\969" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QωOrigin))))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata QωOrigin

Origin of Quantityω.

Constructors

QωInferred
User wrote nothing.
Qω Range
User wrote "@ω".
QωPlenty Range
User wrote "@plenty".

Instances14Eq, Ord, Show, Generic, Semigroup, Monoid, …

Eq QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Right-biased composition, because the left quantity acts as context, and the right one as occurrence.
Monoid QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange QωOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj QωOriginDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type Rep QωOrigin = D1 ('MetaData "Q\969Origin" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "Q\969Inferred" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "Q\969" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q\969Plenty" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

typetype RString = Ranged RawName

String with range info.

datadata Ranged a

Thing with range info.

Constructors

Ranged
- rangeOf :: Range
- rangedThing :: a

Instances45Functor, Foldable, Traversable, Decoration, MapNamedArgPattern, Eq, …

Functor RangedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Foldable RangedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Traversable RangedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
MapNamedArgPattern NAPDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
Decoration RangedDefined in Agda-2.8.0.2 · Agda.Syntax.Common
MapNamedArgPattern a (NamedArg (Pattern' a))Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
Modify the content of VarP, and the closest surrounding NamedArg.
Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.
Eq a => Eq (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ignores range.
Ord a => Ord (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ignores range.
Show a => Show (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData a => NFData (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ranges are not forced.
Pretty a => Pretty (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ignores range.
Pretty e => Pretty (Named_ e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
IsNoName a => IsNoName (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
HasRange (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
DeBruijn a => DeBruijn (Named_ a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute.DeBruijn
Subst a => Subst (Ranged a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
PrettyTCM (NamedArg Expr)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (NamedArg Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Named_ Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
ToConcrete (SplitPattern (NamedArg Pattern))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete (UserPattern (NamedArg Pattern))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete a => ToConcrete (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Normalise t => Normalise (Ranged t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Free t => Free (Ranged t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy
ToAbstract c => ToAbstract (Ranged c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
Hilite a => Hilite (Ranged a)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
Apply [NamedArg (Pattern' a)]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
Make sure we only drop variable patterns.
KillRange (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ExprLike a => ExprLike (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (Ranged a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Generic
PatternVars (NamedArg (Pattern' a))Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
EnsureNoLetStms a => EnsureNoLetStms (NamedArg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
EnsureNoLetStms a => EnsureNoLetStms (Named_ a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
NormaliseProjP a => NormaliseProjP (Named_ a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Records
EmbPrj a => EmbPrj (Ranged a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
IApplyVars p => IApplyVars (NamedArg p)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Telescope.Path
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause
AddContext (List1 (NamedArg Name), Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext ([NamedArg Name], Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
type SubstArg (Ranged a) = SubstArg aDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
type ConOfAbs (Ranged a) = Ranged (ConOfAbs a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ConOfAbs (SplitPattern (NamedArg Pattern)) = NamedArg PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ConOfAbs (UserPattern (NamedArg Pattern)) = NamedArg PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type AbsOfCon (Ranged c) = Ranged (AbsOfCon c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
type PatternVarOut (NamedArg (Pattern' a)) = aDefined in Agda-2.8.0.2 · Agda.Syntax.Internal

typetype RawName = String

A RawName is some sort of string.

datadata RecordDirectives' a

Constructors

RecordDirectives
- recInductive :: Maybe (Ranged Induction)
- recHasEta :: Maybe (Ranged HasEta0)
- recPattern :: Maybe Range
- recConstructor :: a

Instances14Functor, Foldable, Traversable, ToConcrete, Hilite, DeclaredNames, …

Functor RecordDirectives'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Foldable RecordDirectives'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Traversable RecordDirectives'Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ToConcrete RecordDirectivesDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Hilite RecordDirectivesDefined in Agda-2.8.0.2 · 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
- -------------------------------------------------------------------- | 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.8.0.2 · Agda.Syntax.Abstract.Views
Eq a => Eq (RecordDirectives' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Show a => Show (RecordDirectives' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData a => NFData (RecordDirectives' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Null a => Null (RecordDirectives' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange a => HasRange (RecordDirectives' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange a => KillRange (RecordDirectives' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj a => EmbPrj (RecordDirectives' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
type ConOfAbs RecordDirectives = [RecordDirective]Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete

datadata Relevance

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

Constructors

Relevant OriginRelevant
The argument is (possibly) relevant at compile-time.
ShapeIrrelevant OriginShapeIrrelevant
Like Quantity0, the argument may never flow into evaluation position. So it is irrelevant at run-time, yet treated relevantly during equality checking.
Unlike Quantity0, it is used to type Irrelevant arguments in functions: 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 OriginIrrelevant
The argument is irrelevant at compile- and runtime.

Instances26Eq, Ord, Show, Generic, NFData, Pretty, …

Eq RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
More relevant is smaller.
Show RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Null RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
null means no information, not even origin or range.
HasRange RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PrettyTCM RelevanceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
Verbalize RelevanceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Errors
LensRelevance RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
PartialOrd RelevanceDefined in Agda-2.8.0.2 · Agda.Syntax.Common
More relevant is smaller.
EmbPrj RelevanceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
Unquote RelevanceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Semigroup (UnderAddition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup (UnderComposition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Relevance forms a semigroup under composition.
Monoid (UnderAddition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid (UnderComposition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Relevant is the unit under composition.
LeftClosedPOMonoid (UnderComposition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderAddition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderComposition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderAddition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderComposition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep Relevance = D1 ('MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "Relevant" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OriginRelevant)) :+: (C1 ('MetaCons "ShapeIrrelevant" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OriginShapeIrrelevant)) :+: C1 ('MetaCons "Irrelevant" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OriginIrrelevant))))Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata Renaming' n m

Constructors

Renaming
- renFrom :: ImportedName' n m
  Rename from this name.
- renTo :: ImportedName' n m
  To this one. Must be same kind as renFrom.
- renFixity :: Maybe Fixity
  New fixity of renTo (optional).
- renToRange :: Range
  The range of the "to" keyword. Retained for highlighting purposes.

Instances7Eq, Show, NFData, Pretty, HasRange, Hilite, …

(Eq m, Eq n) => Eq (Renaming' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Show m, Show n) => Show (Renaming' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(NFData a, NFData b) => NFData (Renaming' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ranges are not forced.
(Pretty a, Pretty b) => Pretty (Renaming' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange a, HasRange b) => HasRange (Renaming' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Hilite m, Hilite n, Hilite (RenamingTo m), Hilite (RenamingTo n)) => Hilite (Renaming' m n)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
(KillRange a, KillRange b) => KillRange (Renaming' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

typetype RenamingDirective' n m = [Renaming' n m]

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

Rewrite (List1 (qn, e))
```
rewrite e
```
Invert qn (List1 (Named nm (p, e)))
```
with p <- e in eq
```
LeftLet (List1 (p, e))
```
using p <- e
```

Instances19Functor, Foldable, Traversable, Eq, Show, NFData, …

ToAbstract RewriteEqnDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
Functor (RewriteEqn' qn nm p)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Foldable (RewriteEqn' qn nm p)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Traversable (RewriteEqn' qn nm p)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Eq qn, Eq nm, Eq p, Eq e) => Eq (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Show qn, Show nm, Show p, Show e) => Show (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(NFData qn, NFData nm, NFData p, NFData e) => NFData (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Pretty nm, Pretty p, Pretty e) => Pretty (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToAbstract (RewriteEqn' () BindName Pattern Expr)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
(HasRange n, Hilite p, Hilite e) => Hilite (RewriteEqn' x n p e)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
(KillRange qn, KillRange nm, KillRange e, KillRange p) => KillRange (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(BoundAndUsed x, BoundAndUsed p, BoundAndUsed e) => BoundAndUsed (RewriteEqn' q x p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.UsedNames
(ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Generic
type ConOfAbs (RewriteEqn' qn BindName p a) = RewriteEqn' () Name (ConOfAbs p) (ConOfAbs a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqnDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

datadata TerminationCheck m

Termination check? (Default = TerminationCheck).

Constructors

TerminationCheck
Run the termination checker.
NoTerminationCheck
Skip termination checking (unsafe).
NonTerminating
Treat as non-terminating.
Terminating
Treat as terminating (unsafe). Same effect as NoTerminationCheck.
TerminationMeasure Range m
Skip termination checking but use measure instead.

Instances5Functor, Eq, Show, NFData, KillRange

Functor TerminationCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq m => Eq (TerminationCheck m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Show m => Show (TerminationCheck m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData a => NFData (TerminationCheck a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange m => KillRange (TerminationCheck m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

newtypenewtype UnderAddition t

Type wrapper to indicate additive monoid/semigroup context.

Constructors

UnderAddition t

Instances26Functor, Applicative, Eq, Ord, Show, Semigroup, …

Functor UnderAdditionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Applicative UnderAdditionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq t => Eq (UnderAddition t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord t => Ord (UnderAddition t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Show t => Show (UnderAddition t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup (UnderAddition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Cohesion forms a semigroup under addition.
Semigroup (UnderAddition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pointwise addition.
Semigroup (UnderAddition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ModalPolarity forms a semigroup under addition.
Semigroup (UnderAddition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup (UnderAddition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid (UnderAddition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Squash is the additive unit.
Monoid (UnderAddition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pointwise additive unit.
Monoid (UnderAddition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
'' is the additive unit.
Monoid (UnderAddition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid (UnderAddition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderAddition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderAddition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderAddition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderAddition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderAddition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderAddition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderAddition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderAddition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderAddition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderAddition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
PartialOrd t => PartialOrd (UnderAddition t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

newtypenewtype UnderComposition t

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

Constructors

UnderComposition t

Instances32Functor, Applicative, Eq, Ord, Show, Semigroup, …

Functor UnderCompositionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Applicative UnderCompositionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq t => Eq (UnderComposition t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord t => Ord (UnderComposition t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Show t => Show (UnderComposition t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup (UnderComposition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Cohesion forms a semigroup under composition.
Semigroup (UnderComposition Erased)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup (UnderComposition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pointwise composition.
Semigroup (UnderComposition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ModalPolarity forms a semigroup under composition.
Semigroup (UnderComposition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Composition of quantities (multiplication).
Quantity0 is dominant. Quantity1 is neutral.
Right-biased for origin.
Semigroup (UnderComposition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Relevance forms a semigroup under composition.
Monoid (UnderComposition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Continous is the multiplicative unit.
Monoid (UnderComposition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pointwise composition unit.
Monoid (UnderComposition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Continous is the multiplicative unit.
Monoid (UnderComposition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
In the absense of finite quantities besides 0, ω is the unit. Otherwise, 1 is the unit.
Monoid (UnderComposition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Relevant is the unit under composition.
LeftClosedPOMonoid (UnderComposition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LeftClosedPOMonoid (UnderComposition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LeftClosedPOMonoid (UnderComposition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LeftClosedPOMonoid (UnderComposition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
LeftClosedPOMonoid (UnderComposition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderComposition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderComposition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderComposition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderComposition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POMonoid (UnderComposition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderComposition Cohesion)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderComposition Modality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderComposition PolarityModality)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderComposition Quantity)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
POSemigroup (UnderComposition Relevance)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
PartialOrd t => PartialOrd (UnderComposition t)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

classclass Eq a => Underscore a where

Methods

underscore :: a
isUnderscore :: a -> Bool

Instances6Underscore

Underscore ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
Underscore DocDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Underscore NameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Underscore QNameDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
Underscore ByteStringDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Underscore StringDefined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata UniverseCheck

Universe check? (Default is yes).

YesUniverseCheck NoUniverseCheck

Instances9Bounded, Enum, Eq, Ord, Show, Generic, …

Bounded UniverseCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Enum UniverseCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq UniverseCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord UniverseCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show UniverseCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Generic UniverseCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData UniverseCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
KillRange UniverseCheckDefined in Agda-2.8.0.2 · Agda.Syntax.Common
type Rep UniverseCheck = D1 ('MetaData "UniverseCheck" "Agda.Syntax.Common" "Agda-2.8.0.2-IWATId8XtJVEb9GRZaI6YB" 'False) (C1 ('MetaCons "YesUniverseCheck" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NoUniverseCheck" 'PrefixI 'False) U1)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata Using' n m

The using clause of import directive.

Constructors

UseEverything
No using clause given.
Using [ImportedName' n m]
using the specified names.

Instances10Eq, Show, Semigroup, Monoid, NFData, Pretty, …

(Eq m, Eq n) => Eq (Using' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Show m, Show n) => Show (Using' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup (Using' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Monoid (Using' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(NFData a, NFData b) => NFData (Using' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Pretty a, Pretty b) => Pretty (Using' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Null (Using' n m)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(HasRange a, HasRange b) => HasRange (Using' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
(Hilite m, Hilite n) => Hilite (Using' m n)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
(KillRange a, KillRange b) => KillRange (Using' a b)Defined in Agda-2.8.0.2 · Agda.Syntax.Common

datadata WithHiding a

Decorating something with Hiding information.

Constructors

WithHiding
- whHiding :: !Hiding
- whThing :: a

Instances30Functor, Applicative, Foldable, Traversable, Decoration, Eq, …

Functor WithHidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Applicative WithHidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Foldable WithHidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Traversable WithHidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Decoration WithHidingDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Eq a => Eq (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord a => Ord (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Show a => Show (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData a => NFData (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty a => Pretty (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
HasRange a => HasRange (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Subst a => Subst (WithHiding a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
PrettyTCM a => PrettyTCM (WithHiding a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
ToConcrete a => ToConcrete (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Normalise t => Normalise (WithHiding t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce
Free t => Free (WithHiding t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.Lazy
ToAbstract c => ToAbstract (WithHiding c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
Hilite a => Hilite (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
LensHiding (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
TermLike a => TermLike (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Generic
KillRange a => KillRange (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange a => SetRange (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
ExprLike a => ExprLike (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
ExprLike a => ExprLike (WithHiding a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Generic
EmbPrj a => EmbPrj (WithHiding a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
AddContext (List1 (WithHiding Name), Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext ([WithHiding Name], Dom Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
type SubstArg (WithHiding a) = SubstArg aDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
type ConOfAbs (WithHiding a) = WithHiding (ConOfAbs a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type AbsOfCon (WithHiding c) = WithHiding (AbsOfCon c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

datadata WithOrigin a

Decorating something with Origin information.

Constructors

WithOrigin
- woOrigin :: !Origin
- woThing :: a

Instances36Functor, Foldable, Traversable, Decoration, MapNamedArgPattern, Eq, …

Functor WithOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Foldable WithOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Traversable WithOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
MapNamedArgPattern NAPDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Pattern
Decoration WithOriginDefined in Agda-2.8.0.2 · Agda.Syntax.Common
MapNamedArgPattern a (NamedArg (Pattern' a))Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.Pattern
Modify the content of VarP, and the closest surrounding NamedArg.
Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.
Eq a => Eq (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Ord a => Ord (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Show a => Show (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
NFData a => NFData (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty a => Pretty (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Pretty e => Pretty (Named_ e)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
IsNoName a => IsNoName (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Name
HasRange a => HasRange (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
DeBruijn a => DeBruijn (Named_ a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute.DeBruijn
PrettyTCM (NamedArg Expr)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (NamedArg Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
PrettyTCM (Named_ Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Pretty
ToConcrete (SplitPattern (NamedArg Pattern))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
ToConcrete (UserPattern (NamedArg Pattern))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
LensOrigin (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
Apply [NamedArg (Pattern' a)]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan
Make sure we only drop variable patterns.
KillRange a => KillRange (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
SetRange a => SetRange (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.Syntax.Common
PatternVars (NamedArg (Pattern' a))Defined in Agda-2.8.0.2 · Agda.Syntax.Internal
EnsureNoLetStms a => EnsureNoLetStms (NamedArg a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
EnsureNoLetStms a => EnsureNoLetStms (Named_ a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
NormaliseProjP a => NormaliseProjP (Named_ a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Records
EmbPrj a => EmbPrj (WithOrigin a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan
IApplyVars p => IApplyVars (NamedArg p)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Telescope.Path
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.Clause
AddContext (List1 (NamedArg Name), Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
AddContext ([NamedArg Name], Type)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Context
type ConOfAbs (SplitPattern (NamedArg Pattern)) = NamedArg PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type ConOfAbs (UserPattern (NamedArg Pattern)) = NamedArg PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
type PatternVarOut (NamedArg (Pattern' a)) = aDefined in Agda-2.8.0.2 · Agda.Syntax.Internal

module Agda.Syntax.Common.KeywordRange

module Agda.Syntax.TopLevelModuleName.Boot

datadata Induction

Inductive CoInductive

Instances9Eq, Ord, Show, NFData, Pretty, HasRange, …

Eq InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common.Aspect
Ord InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common.Aspect
Show InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common.Aspect
NFData InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common.Aspect
Pretty InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common · orphan
HasRange InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common · orphan
KillRange InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common · orphan
PatternMatchingAllowed InductionDefined in Agda-2.8.0.2 · Agda.Syntax.Common
EmbPrj InductionDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

Orphan instances

3 instances