Safe Haskell | None |
---|---|
Language | Haskell2010 |
Some common syntactic entities are defined in this module.
Synopsis
- data ImportDirective' n m = ImportDirective {
- importDirRange :: Range
- using :: Using' n m
- hiding :: HidingDirective' n m
- impRenaming :: RenamingDirective' n m
- publicOpen :: Maybe KwRange
- data IsMain
- data Origin
- type Nat = Int
- newtype InteractionId = InteractionId {
- interactionId :: Nat
- data Modality = Modality {}
- newtype ProblemId = ProblemId Nat
- data Fixity = Fixity {}
- data RewriteEqn' qn nm p e
- data MetaId = MetaId {
- metaId :: !Word64
- metaModule :: !ModuleNameHash
- data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
- data Arg e = Arg {}
- data ArgInfo = ArgInfo {}
- defaultArgInfo :: ArgInfo
- data ConOrigin
- data Hiding
- class LensOrigin a where
- data NameId = NameId !Word64 !ModuleNameHash
- data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
- class LensHiding a where
- data ProjOrigin
- data WithOrigin a = WithOrigin {}
- visible :: LensHiding a => a -> Bool
- data TerminationCheck m
- type Notation = [NotationPart]
- data Cohesion
- = Flat
- | Continuous
- | Squash
- data RecordDirectives' a = RecordDirectives {
- recInductive :: Maybe (Ranged Induction)
- recHasEta :: Maybe (Ranged HasEta0)
- recPattern :: Maybe Range
- recConstructor :: Maybe a
- data Using' n m
- = UseEverything
- | Using [ImportedName' n m]
- data ImportedName' n m
- = ImportedModule m
- | ImportedName n
- data Renaming' n m = Renaming {
- renFrom :: ImportedName' n m
- renTo :: ImportedName' n m
- renFixity :: Maybe Fixity
- renToRange :: Range
- data Lock
- data Cubical
- data Language
- type NamedArg a = Arg (Named_ a)
- data IsOpaque
- fromImportedName :: ImportedName' a a -> a
- partitionImportedNames :: [ImportedName' n m] -> ([n], [m])
- defaultArg :: a -> Arg a
- data Relevance
- class LensRelevance a where
- getRelevance :: a -> Relevance
- setRelevance :: Relevance -> a -> a
- mapRelevance :: (Relevance -> Relevance) -> a -> a
- hasQuantity0 :: LensQuantity a => a -> Bool
- data WithHiding a = WithHiding {}
- newtype Constr a = Constr a
- data Associativity
- data OverlapMode
- data Overlappable
- defaultFixity :: Fixity
- isInstance :: LensHiding a => a -> Bool
- type Arity = Nat
- data FileType
- type HasEta0 = HasEta' ()
- emptyRecordDirectives :: RecordDirectives' a
- data HasEta' a
- type HasEta = HasEta' PatternOrCopattern
- data PatternOrCopattern
- class PatternMatchingAllowed a where
- patternMatchingAllowed :: a -> Bool
- class CopatternMatchingAllowed a where
- copatternMatchingAllowed :: a -> Bool
- class HasOverlapMode a where
- isIncoherent :: HasOverlapMode a => a -> Bool
- isOverlappable :: HasOverlapMode a => a -> Bool
- isOverlapping :: HasOverlapMode a => a -> Bool
- hidingToString :: Hiding -> String
- class LensArgInfo a where
- getArgInfo :: a -> ArgInfo
- setArgInfo :: ArgInfo -> a -> a
- mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a
- mergeHiding :: LensHiding a => WithHiding a -> a
- notVisible :: LensHiding a => a -> Bool
- hidden :: LensHiding a => a -> Bool
- hide :: LensHiding a => a -> a
- hideOrKeepInstance :: LensHiding a => a -> a
- makeInstance :: LensHiding a => a -> a
- makeInstance' :: LensHiding a => Overlappable -> a -> a
- isYesOverlap :: LensHiding a => a -> Bool
- sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool
- newtype UnderAddition t = UnderAddition t
- newtype UnderComposition t = UnderComposition t
- data Quantity
- composeModality :: Modality -> Modality -> Modality
- unitModality :: Modality
- inverseComposeModality :: Modality -> Modality -> Modality
- addModality :: Modality -> Modality -> Modality
- zeroModality :: Modality
- moreUsableModality :: Modality -> Modality -> Bool
- usableModality :: LensModality a => a -> Bool
- class LensModality a where
- getModality :: a -> Modality
- setModality :: Modality -> a -> a
- mapModality :: (Modality -> Modality) -> a -> a
- usableRelevance :: LensRelevance a => a -> Bool
- usableQuantity :: LensQuantity a => a -> Bool
- usableCohesion :: LensCohesion a => a -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- composeQuantity :: Quantity -> Quantity -> Quantity
- composeCohesion :: Cohesion -> Cohesion -> Cohesion
- applyModality :: LensModality a => Modality -> a -> a
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- inverseComposeQuantity :: Quantity -> Quantity -> Quantity
- inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion
- inverseApplyModalityButNotQuantity :: LensModality a => Modality -> a -> a
- class LensQuantity a where
- getQuantity :: a -> Quantity
- setQuantity :: Quantity -> a -> a
- mapQuantity :: (Quantity -> Quantity) -> a -> a
- data Q1Origin
- = Q1Inferred
- | Q1 Range
- | Q1Linear Range
- addRelevance :: Relevance -> Relevance -> Relevance
- addQuantity :: Quantity -> Quantity -> Quantity
- addCohesion :: Cohesion -> Cohesion -> Cohesion
- zeroRelevance :: Relevance
- zeroQuantity :: Quantity
- zeroCohesion :: Cohesion
- unitRelevance :: Relevance
- unitQuantity :: Quantity
- unitCohesion :: Cohesion
- topModality :: Modality
- topRelevance :: Relevance
- topQuantity :: Quantity
- topCohesion :: Cohesion
- defaultModality :: Modality
- defaultRelevance :: Relevance
- defaultQuantity :: Quantity
- defaultCohesion :: Cohesion
- sameModality :: (LensModality a, LensModality b) => a -> b -> Bool
- sameRelevance :: Relevance -> Relevance -> Bool
- sameQuantity :: Quantity -> Quantity -> Bool
- sameCohesion :: Cohesion -> Cohesion -> Bool
- lModRelevance :: Lens' Modality Relevance
- lModQuantity :: Lens' Modality Quantity
- lModCohesion :: Lens' Modality Cohesion
- class LensCohesion a where
- getCohesion :: a -> Cohesion
- setCohesion :: Cohesion -> a -> a
- mapCohesion :: (Cohesion -> Cohesion) -> a -> a
- getRelevanceMod :: LensModality a => LensGet a Relevance
- setRelevanceMod :: LensModality a => LensSet a Relevance
- mapRelevanceMod :: LensModality a => LensMap a Relevance
- getQuantityMod :: LensModality a => LensGet a Quantity
- setQuantityMod :: LensModality a => LensSet a Quantity
- mapQuantityMod :: LensModality a => LensMap a Quantity
- getCohesionMod :: LensModality a => LensGet a Cohesion
- setCohesionMod :: LensModality a => LensSet a Cohesion
- mapCohesionMod :: LensModality a => LensMap a Cohesion
- data Q0Origin
- = Q0Inferred
- | Q0 Range
- | Q0Erased Range
- data QωOrigin
- = QωInferred
- | Qω Range
- | QωPlenty Range
- moreQuantity :: Quantity -> Quantity -> Bool
- applyQuantity :: LensQuantity a => Quantity -> a -> a
- inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a
- hasQuantity1 :: LensQuantity a => a -> Bool
- hasQuantityω :: LensQuantity a => a -> Bool
- noUserQuantity :: LensQuantity a => a -> Bool
- isQuantityω :: LensQuantity a => a -> Bool
- data Erased
- defaultErased :: Erased
- asQuantity :: Erased -> Quantity
- erasedFromQuantity :: Quantity -> Maybe Erased
- sameErased :: Erased -> Erased -> Bool
- isErased :: Erased -> Bool
- composeErased :: Erased -> Erased -> Erased
- allRelevances :: [Relevance]
- isRelevant :: LensRelevance a => a -> Bool
- isIrrelevant :: LensRelevance a => a -> Bool
- isNonStrict :: LensRelevance a => a -> Bool
- moreRelevant :: Relevance -> Relevance -> Bool
- applyRelevance :: LensRelevance a => Relevance -> a -> a
- inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToRel :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- data Annotation = Annotation {}
- defaultAnnotation :: Annotation
- defaultLock :: Lock
- class LensAnnotation a where
- getAnnotation :: a -> Annotation
- setAnnotation :: Annotation -> a -> a
- mapAnnotation :: (Annotation -> Annotation) -> a -> a
- data LockOrigin
- class LensLock a where
- allCohesions :: [Cohesion]
- isContinuous :: LensCohesion a => a -> Bool
- moreCohesion :: Cohesion -> Cohesion -> Bool
- applyCohesion :: LensCohesion a => Cohesion -> a -> a
- inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a
- data FreeVariables
- = UnknownFVs
- | KnownFVs IntSet
- unknownFreeVariables :: FreeVariables
- noFreeVariables :: FreeVariables
- oneFreeVariable :: Int -> FreeVariables
- freeVariablesFromList :: [Int] -> FreeVariables
- class LensFreeVariables a where
- getFreeVariables :: a -> FreeVariables
- setFreeVariables :: FreeVariables -> a -> a
- mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a
- hasNoFreeVariables :: LensFreeVariables a => a -> Bool
- getHidingArgInfo :: LensArgInfo a => LensGet a Hiding
- setHidingArgInfo :: LensArgInfo a => LensSet a Hiding
- mapHidingArgInfo :: LensArgInfo a => LensMap a Hiding
- getModalityArgInfo :: LensArgInfo a => LensGet a Modality
- setModalityArgInfo :: LensArgInfo a => LensSet a Modality
- mapModalityArgInfo :: LensArgInfo a => LensMap a Modality
- getOriginArgInfo :: LensArgInfo a => LensGet a Origin
- setOriginArgInfo :: LensArgInfo a => LensSet a Origin
- mapOriginArgInfo :: LensArgInfo a => LensMap a Origin
- getFreeVariablesArgInfo :: LensArgInfo a => LensGet a FreeVariables
- setFreeVariablesArgInfo :: LensArgInfo a => LensSet a FreeVariables
- mapFreeVariablesArgInfo :: LensArgInfo a => LensMap a FreeVariables
- isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool
- withArgsFrom :: [a] -> [Arg b] -> [Arg a]
- withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a]
- class Eq a => Underscore a where
- underscore :: a
- isUnderscore :: a -> Bool
- type Named_ = Named NamedName
- type NamedName = WithOrigin (Ranged ArgName)
- type ArgName = String
- sameName :: NamedName -> NamedName -> Bool
- unnamed :: a -> Named name a
- isUnnamed :: Named name a -> Maybe a
- named :: name -> a -> Named name a
- userNamed :: Ranged ArgName -> a -> Named_ a
- class LensNamed a where
- type family NameOf a
- getNameOf :: LensNamed a => a -> Maybe (NameOf a)
- setNameOf :: LensNamed a => Maybe (NameOf a) -> a -> a
- mapNameOf :: LensNamed a => (Maybe (NameOf a) -> Maybe (NameOf a)) -> a -> a
- bareNameOf :: (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
- bareNameWithDefault :: (LensNamed a, NameOf a ~ NamedName) => ArgName -> a -> ArgName
- namedSame :: (LensNamed a, LensNamed b, NameOf a ~ NamedName, NameOf b ~ NamedName) => a -> b -> Bool
- fittingNamedArg :: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) => arg -> dom -> Maybe Bool
- namedArg :: NamedArg a -> a
- defaultNamedArg :: a -> NamedArg a
- unnamedArg :: ArgInfo -> a -> NamedArg a
- updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
- updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b)
- setNamedArg :: NamedArg a -> b -> NamedArg b
- argNameToString :: ArgName -> String
- stringToArgName :: String -> ArgName
- appendArgNames :: ArgName -> ArgName -> ArgName
- unranged :: a -> Ranged a
- type RawName = String
- rawNameToString :: RawName -> String
- stringToRawName :: String -> RawName
- type RString = Ranged RawName
- bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin
- data IsInfix
- data Access
- privateAccessInserted :: Access
- data IsAbstract
- class LensIsAbstract a where
- class AnyIsAbstract a where
- anyIsAbstract :: a -> IsAbstract
- data IsInstance
- data IsMacro
- data OpaqueId = OpaqueId !Word64 !ModuleNameHash
- class LensIsOpaque a where
- lensIsOpaque :: Lens' a IsOpaque
- data JointOpacity
- = UniqueOpaque !OpaqueId
- | DifferentOpaque !(HashSet OpaqueId)
- | NoOpaque
- class AllAreOpaque a where
- jointOpacity :: a -> JointOpacity
- data PositionInName
- data MaybePlaceholder e
- noPlaceholder :: e -> MaybePlaceholder e
- type PrecedenceLevel = Double
- data FixityLevel
- noFixity :: Fixity
- data Fixity' = Fixity' {
- theFixity :: !Fixity
- theNotation :: Notation
- theNameRange :: Range
- noFixity' :: Fixity'
- noNotation :: Notation
- _fixityAssoc :: Lens' Fixity Associativity
- _fixityLevel :: Lens' Fixity FixityLevel
- class LensFixity a where
- lensFixity :: Lens' a Fixity
- class LensFixity' a where
- lensFixity' :: Lens' a Fixity'
- type HidingDirective' n m = [ImportedName' n m]
- type RenamingDirective' n m = [Renaming' n m]
- defaultImportDir :: ImportDirective' n m
- isDefaultImportDir :: ImportDirective' n m -> Bool
- mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2
- setImportedName :: ImportedName' a a -> a -> ImportedName' a a
- data PositivityCheck
- data UniverseCheck
- data CoverageCheck
- data ExpandedEllipsis
- = ExpandedEllipsis {
- ellipsisRange :: Range
- ellipsisWithArgs :: Int
- | NoEllipsis
- = ExpandedEllipsis {
- data NotationPart
- data BoundVariablePosition = BoundVariablePosition {
- holeNumber :: !Int
- varNumber :: !Int
- module Agda.Syntax.Common.KeywordRange
- module Agda.Syntax.TopLevelModuleName.Boot
- data Induction
Documentation
data ImportDirective' n m Source #
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import
, namespace
, or open
declarations).
ImportDirective | |
|
Instances
Origin of arguments.
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 |
Instances
LensOrigin Origin Source # | |
HasRange Origin Source # | |
KillRange Origin Source # | |
Defined in Agda.Syntax.Common | |
ChooseFlex Origin Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: Origin -> Origin -> FlexChoice Source # | |
EmbPrj Origin Source # | |
NFData Origin Source # | |
Defined in Agda.Syntax.Common | |
Show Origin Source # | |
Eq Origin Source # | |
Ord Origin Source # | |
newtype InteractionId Source #
Instances
We have a tuple of modalities, which might not be fully orthogonal. For example, irrelevant stuff is also run-time irrelevant.
Modality | |
|
Instances
LensCohesion Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
LensModality Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
LensQuantity Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
LensRelevance Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
Pretty Modality Source # | |||||
HasRange Modality Source # | |||||
KillRange Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
Verbalize Modality Source # | |||||
Defined in Agda.TypeChecking.Errors | |||||
PrettyTCM Modality Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
EmbPrj Modality Source # | |||||
Unquote Modality Source # | |||||
PartialOrd Modality Source # | Dominance ordering. | ||||
Defined in Agda.Syntax.Common | |||||
NFData Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic Modality Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show Modality Source # | |||||
Eq Modality Source # | |||||
Ord Modality Source # | |||||
IsVarSet () AllowedVar Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Occurs withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar Source # | |||||
LeftClosedPOMonoid (UnderComposition Modality) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POMonoid (UnderAddition Modality) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POMonoid (UnderComposition Modality) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POSemigroup (UnderAddition Modality) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POSemigroup (UnderComposition Modality) Source # | |||||
Defined in Agda.Syntax.Common | |||||
Monoid (UnderAddition Modality) Source # | Pointwise additive unit. | ||||
Defined in Agda.Syntax.Common | |||||
Monoid (UnderComposition Modality) Source # | Pointwise composition unit. | ||||
Semigroup (UnderAddition Modality) Source # | Pointwise addition. | ||||
Defined in Agda.Syntax.Common (<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality # sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality | |||||
Semigroup (UnderComposition Modality) Source # | Pointwise composition. | ||||
Defined in Agda.Syntax.Common (<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality # sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality | |||||
type Rep Modality Source # | |||||
Defined in Agda.Syntax.Common type Rep Modality = D1 ('MetaData "Modality" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" '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)))) |
A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.
Instances
EncodeTCM ProblemId Source # | |
Pretty ProblemId Source # | |
HasFresh ProblemId Source # | |
PrettyTCM ProblemId Source # | |
Defined in Agda.TypeChecking.Pretty | |
EmbPrj ProblemId Source # | |
NFData ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Enum ProblemId Source # | |
Num ProblemId Source # | |
Integral ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Real ProblemId Source # | |
Defined in Agda.Syntax.Common toRational :: ProblemId -> Rational | |
Show ProblemId Source # | |
Eq ProblemId Source # | |
Ord ProblemId Source # | |
Defined in Agda.Syntax.Common | |
ToJSON ProblemId Source # | |
Defined in Agda.Interaction.JSONTop | |
Monad m => MonadFresh ProblemId (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure fresh :: PureConversionT m ProblemId Source # |
Fixity of operators.
Fixity | |
|
Instances
LensFixity Fixity Source # | |
Defined in Agda.Syntax.Common | |
Pretty Fixity Source # | |
HasRange Fixity Source # | |
KillRange Fixity Source # | |
Defined in Agda.Syntax.Common | |
ToTerm Fixity Source # | |
EmbPrj Fixity Source # | |
Null Fixity Source # | |
NFData Fixity Source # | |
Defined in Agda.Syntax.Common | |
Show Fixity Source # | |
Eq Fixity Source # | |
Ord Fixity Source # | |
data RewriteEqn' qn nm p e Source #
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
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 |
Instances
ToAbstract RewriteEqn Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source # | |||||
Functor (RewriteEqn' qn nm p) Source # | |||||
Defined in Agda.Syntax.Common fmap :: (a -> b) -> RewriteEqn' qn nm p a -> RewriteEqn' qn nm p b (<$) :: a -> RewriteEqn' qn nm p b -> RewriteEqn' qn nm p a # | |||||
Foldable (RewriteEqn' qn nm p) Source # | |||||
Defined in Agda.Syntax.Common fold :: Monoid m => RewriteEqn' qn nm p m -> m foldMap :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m foldMap' :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m foldr :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b foldr' :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b foldl :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b foldl' :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b foldr1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a foldl1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a toList :: RewriteEqn' qn nm p a -> [a] null :: RewriteEqn' qn nm p a -> Bool length :: RewriteEqn' qn nm p a -> Int elem :: Eq a => a -> RewriteEqn' qn nm p a -> Bool maximum :: Ord a => RewriteEqn' qn nm p a -> a minimum :: Ord a => RewriteEqn' qn nm p a -> a sum :: Num a => RewriteEqn' qn nm p a -> a product :: Num a => RewriteEqn' qn nm p a -> a | |||||
Traversable (RewriteEqn' qn nm p) Source # | |||||
Defined in Agda.Syntax.Common traverse :: Applicative f => (a -> f b) -> RewriteEqn' qn nm p a -> f (RewriteEqn' qn nm p b) sequenceA :: Applicative f => RewriteEqn' qn nm p (f a) -> f (RewriteEqn' qn nm p a) mapM :: Monad m => (a -> m b) -> RewriteEqn' qn nm p a -> m (RewriteEqn' qn nm p b) sequence :: Monad m => RewriteEqn' qn nm p (m a) -> m (RewriteEqn' qn nm p a) | |||||
(ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m (RewriteEqn' qn nm p e) Source # foldExpr :: FoldExprFn m (RewriteEqn' qn nm p e) Source # traverseExpr :: TraverseExprFn m (RewriteEqn' qn nm p e) Source # mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e Source # | |||||
(Pretty nm, Pretty p, Pretty e) => Pretty (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Common pretty :: RewriteEqn' qn nm p e -> Doc Source # prettyPrec :: Int -> RewriteEqn' qn nm p e -> Doc Source # prettyList :: [RewriteEqn' qn nm p e] -> Doc Source # | |||||
(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Concrete.Generic mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e Source # foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn nm p e -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e) Source # | |||||
(HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Common getRange :: RewriteEqn' qn nm p e -> Range Source # | |||||
(KillRange qn, KillRange nm, KillRange e, KillRange p) => KillRange (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Common killRange :: KillRangeT (RewriteEqn' qn nm p e) Source # | |||||
(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: RewriteEqn' qn BindName p a -> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a)) Source # bindToConcrete :: RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> AbsToCon b) -> AbsToCon b Source # | |||||
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source # | |||||
(NFData qn, NFData nm, NFData p, NFData e) => NFData (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Common rnf :: RewriteEqn' qn nm p e -> () | |||||
(Show e, Show qn, Show nm, Show p) => Show (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> RewriteEqn' qn nm p e -> ShowS show :: RewriteEqn' qn nm p e -> String showList :: [RewriteEqn' qn nm p e] -> ShowS | |||||
(Eq e, Eq qn, Eq nm, Eq p) => Eq (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Common (==) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool (/=) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool | |||||
type AbsOfCon RewriteEqn Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
type ConOfAbs (RewriteEqn' qn BindName p a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Meta-variable identifiers use the same structure as NameId
s.
MetaId | |
|
Instances
EncodeTCM MetaId Source # | |||||
Pretty MetaId Source # | |||||
GetDefs MetaId Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => MetaId -> m () Source # | |||||
NamesIn MetaId Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
Reify MetaId Source # | |||||
HasFresh MetaId Source # | |||||
IsInstantiatedMeta MetaId Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source # | |||||
UnFreezeMeta MetaId Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source # | |||||
PrettyTCM MetaId Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
FromTerm MetaId Source # | |||||
Defined in Agda.TypeChecking.Primitive | |||||
PrimTerm MetaId Source # | |||||
PrimType MetaId Source # | |||||
ToTerm MetaId Source # | |||||
EmbPrj MetaId Source # | |||||
Unquote MetaId Source # | |||||
NFData MetaId Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum MetaId Source # | |||||
Generic MetaId Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show MetaId Source # | The record selectors are not included in the resulting strings. | ||||
Eq MetaId Source # | |||||
Ord MetaId Source # | |||||
Hashable MetaId Source # | |||||
Defined in Agda.Syntax.Common hashWithSalt :: Int -> MetaId -> Int | |||||
ToJSON MetaId Source # | |||||
Defined in Agda.Interaction.JSONTop | |||||
Singleton MetaId MetaSet Source # | |||||
Singleton MetaId () Source # | |||||
Defined in Agda.TypeChecking.Free.Lazy | |||||
InstantiateFull (Judgement MetaId) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
type ReifiesTo MetaId Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type Rep MetaId Source # | |||||
Defined in Agda.Syntax.Common type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Just "metaModule") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash))) |
Thing with range info.
Ranged | |
|
Instances
MapNamedArgPattern NAP Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
Decoration Ranged Source # | |||||
Functor Ranged Source # | |||||
Foldable Ranged Source # | |||||
Defined in Agda.Syntax.Common fold :: Monoid m => Ranged m -> m foldMap :: Monoid m => (a -> m) -> Ranged a -> m foldMap' :: Monoid m => (a -> m) -> Ranged a -> m foldr :: (a -> b -> b) -> b -> Ranged a -> b foldr' :: (a -> b -> b) -> b -> Ranged a -> b foldl :: (b -> a -> b) -> b -> Ranged a -> b foldl' :: (b -> a -> b) -> b -> Ranged a -> b foldr1 :: (a -> a -> a) -> Ranged a -> a foldl1 :: (a -> a -> a) -> Ranged a -> a elem :: Eq a => a -> Ranged a -> Bool maximum :: Ord a => Ranged a -> a | |||||
Traversable Ranged Source # | |||||
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
ExprLike a => ExprLike (Ranged a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m (Ranged a) Source # foldExpr :: FoldExprFn m (Ranged a) Source # traverseExpr :: TraverseExprFn m (Ranged a) Source # | |||||
Pretty e => Pretty (Named_ e) Source # | |||||
Pretty a => Pretty (Ranged a) Source # | Ignores range. | ||||
ExprLike a => ExprLike (Ranged a) Source # | |||||
IsNoName a => IsNoName (Ranged a) Source # | |||||
Defined in Agda.Syntax.Concrete.Name | |||||
PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal
patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source # | |||||
HasRange (Ranged a) Source # | |||||
KillRange (Ranged a) Source # | |||||
Defined in Agda.Syntax.Common killRange :: KillRangeT (Ranged a) Source # | |||||
ToConcrete a => ToConcrete (Ranged a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
ToAbstract c => ToAbstract (Ranged c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
| |||||
PrettyTCM (NamedArg Expr) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (NamedArg Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Named_ Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
NormaliseProjP a => NormaliseProjP (Named_ a) Source # | |||||
Defined in Agda.TypeChecking.Records normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source # | |||||
EmbPrj a => EmbPrj (Ranged a) Source # | |||||
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
DeBruijn a => DeBruijn (Named_ a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn deBruijnVar :: Int -> Named_ a Source # debruijnNamedVar :: String -> Int -> Named_ a Source # deBruijnView :: Named_ a -> Maybe Int Source # | |||||
IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path iApplyVars :: NamedArg p -> [Int] Source # | |||||
NFData a => NFData (Ranged a) Source # | Ranges are not forced. | ||||
Defined in Agda.Syntax.Common | |||||
Show a => Show (Ranged a) Source # | |||||
Eq a => Eq (Ranged a) Source # | Ignores range. | ||||
Ord a => Ord (Ranged a) Source # | Ignores range. | ||||
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type ConOfAbs (Ranged a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type AbsOfCon (Ranged c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Instances
MapNamedArgPattern NAP Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
IsPrefixOf Args Source # | |||||
Defined in Agda.TypeChecking.Abstract | |||||
Decoration Arg Source # | |||||
Functor Arg Source # | |||||
Foldable Arg Source # | |||||
Defined in Agda.Syntax.Common fold :: Monoid m => Arg m -> m foldMap :: Monoid m => (a -> m) -> Arg a -> m foldMap' :: Monoid m => (a -> m) -> Arg a -> m foldr :: (a -> b -> b) -> b -> Arg a -> b foldr' :: (a -> b -> b) -> b -> Arg a -> b foldl :: (b -> a -> b) -> b -> Arg a -> b foldl' :: (b -> a -> b) -> b -> Arg a -> b foldr1 :: (a -> a -> a) -> Arg a -> a foldl1 :: (a -> a -> a) -> Arg a -> a elem :: Eq a => a -> Arg a -> Bool maximum :: Ord a => Arg a -> a | |||||
Traversable Arg Source # | |||||
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
PatternLike a b => PatternLike a (Arg b) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
SubstExpr a => SubstExpr (Arg a) Source # | |||||
IsProjP a => IsProjP (Arg a) Source # | |||||
Defined in Agda.Syntax.Abstract.Name isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |||||
APatternLike a => APatternLike (Arg a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
DeclaredNames a => DeclaredNames (Arg a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views declaredNames :: Collection KName m => Arg a -> m Source # | |||||
ExprLike a => ExprLike (Arg a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m (Arg a) Source # foldExpr :: FoldExprFn m (Arg a) Source # traverseExpr :: TraverseExprFn m (Arg a) Source # | |||||
LensAnnotation (Arg t) Source # | |||||
Defined in Agda.Syntax.Common getAnnotation :: Arg t -> Annotation Source # setAnnotation :: Annotation -> Arg t -> Arg t Source # mapAnnotation :: (Annotation -> Annotation) -> Arg t -> Arg t Source # | |||||
LensArgInfo (Arg a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
LensCohesion (Arg e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
LensFreeVariables (Arg e) Source # | |||||
Defined in Agda.Syntax.Common getFreeVariables :: Arg e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Arg e -> Arg e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e Source # | |||||
LensHiding (Arg e) Source # | |||||
LensLock (Arg t) Source # | |||||
LensModality (Arg e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
LensNamed a => LensNamed (Arg a) Source # | |||||
LensOrigin (Arg e) Source # | |||||
LensQuantity (Arg e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
LensRelevance (Arg e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
Pretty a => Pretty (Arg a) Source # | |||||
ExprLike a => ExprLike (Arg a) Source # | |||||
CPatternLike p => CPatternLike (Arg p) Source # | |||||
Defined in Agda.Syntax.Concrete.Pattern | |||||
IsWithP p => IsWithP (Arg p) Source # | |||||
LensSort a => LensSort (Arg a) Source # | |||||
PatternVars (Arg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal
patternVars :: Arg (Pattern' a) -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)] Source # | |||||
PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal
patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source # | |||||
GetDefs a => GetDefs (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Arg a -> m () Source # | |||||
TermLike a => TermLike (Arg a) Source # | |||||
AllMetas a => AllMetas (Arg a) Source # | |||||
NamesIn a => NamesIn (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
CountPatternVars a => CountPatternVars (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern countPatternVars :: Arg a -> Int Source # | |||||
PatternVarModalities a => PatternVarModalities (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
HasRange a => HasRange (Arg a) Source # | |||||
KillRange a => KillRange (Arg a) Source # | |||||
Defined in Agda.Syntax.Common killRange :: KillRangeT (Arg a) Source # | |||||
SetRange a => SetRange (Arg a) Source # | |||||
ToConcrete a => ToConcrete (Arg a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
ToAbstract c => ToAbstract (Arg c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
| |||||
Reify i => Reify (Arg i) Source # | Skip reification of implicit and irrelevant args if option is off. | ||||
Defined in Agda.Syntax.Translation.InternalToAbstract
| |||||
ToAbstract r => ToAbstract (Arg r) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract
toAbstract :: MonadReflectedToAbstract m => Arg r -> m (AbsOfRef (Arg r)) Source # | |||||
ToAbstract r => ToAbstract [Arg r] Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract
toAbstract :: MonadReflectedToAbstract m => [Arg r] -> m (AbsOfRef [Arg r]) Source # | |||||
AbsTerm a => AbsTerm (Arg a) Source # | |||||
EqualSy a => EqualSy (Arg a) Source # | Ignores irrelevant arguments and modality. (And, of course, origin and free variables). | ||||
Free t => Free (Arg t) Source # | |||||
PrecomputeFreeVars a => PrecomputeFreeVars (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: Arg a -> FV (Arg a) Source # | |||||
(Reduce a, ForceNotFree a) => ForceNotFree (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => Arg a -> m (Arg a) | |||||
UsableModality a => UsableModality (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Arg a -> m Bool Source # | |||||
UsableRelevance a => UsableRelevance (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Arg a -> m Bool Source # | |||||
NoProjectedVar a => NoProjectedVar (Arg a) Source # | |||||
Defined in Agda.TypeChecking.MetaVars noProjectedVar :: Arg a -> Either ProjectedVar () Source # | |||||
ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) Source # | |||||
Defined in Agda.TypeChecking.MetaVars | |||||
MentionsMeta t => MentionsMeta (Arg t) Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Arg t -> Bool Source # | |||||
AnyRigid a => AnyRigid (Arg a) Source # | |||||
Occurs a => Occurs (Arg a) Source # | |||||
IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Arg a -> m Bool Source # | |||||
ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Abstract | |||||
ComputeOccurrences a => ComputeOccurrences (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Positivity occurrences :: Arg a -> OccM OccurrencesBuilder Source # | |||||
PrettyTCM (Arg Expr) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Arg Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Arg Type) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Arg String) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Arg Bool) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (NamedArg Expr) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (NamedArg Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
NormaliseProjP a => NormaliseProjP (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Records normaliseProjP :: HasConstInfo m => Arg a -> m (Arg a) Source # | |||||
Instantiate t => Instantiate (Arg t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull t => InstantiateFull (Arg t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
IsMeta a => IsMeta (Arg a) Source # | |||||
Normalise t => Normalise (Arg t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Reduce t => Reduce (Arg t) Source # | |||||
Simplify t => Simplify (Arg t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
GetMatchables a => GetMatchables (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern getMatchables :: Arg a -> [QName] Source # | |||||
IsFlexiblePattern a => IsFlexiblePattern (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Arg a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Arg a -> m Bool Source # | |||||
EmbPrj a => EmbPrj (Arg a) Source # | |||||
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
Subst a => Subst (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Substitute applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a Source # | |||||
SynEq a => SynEq (Arg a) Source # | |||||
PiApplyM a => PiApplyM (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Telescope piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Arg a -> m Type Source # piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Arg a -> m Type Source # | |||||
IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path iApplyVars :: NamedArg p -> [Int] Source # | |||||
Unquote a => Unquote (Arg a) Source # | |||||
NFData e => NFData (Arg e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
Show e => Show (Arg e) Source # | |||||
Eq e => Eq (Arg e) Source # | |||||
Ord e => Ord (Arg e) Source # | |||||
PatternToExpr p e => PatternToExpr (Arg p) (Arg e) Source # | |||||
LabelPatVars a b => LabelPatVars (Arg a) (Arg b) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern
labelPatVars :: Arg a -> State [PatVarLabel (Arg b)] (Arg b) Source # unlabelPatVars :: Arg b -> Arg a Source # | |||||
TermToPattern a b => TermToPattern (Arg a) (Arg b) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Internal | |||||
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
Match a b => Match (Arg a) (Arg b) Source # | |||||
NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
PatternFrom a b => PatternFrom (Arg a) (Arg b) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
AddContext (List1 (Arg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext ([Arg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # | |||||
AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
type ADotT (Arg a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
type NameOf (Arg a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
type PatternVarOut (Arg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type TypeOf (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type PatVar (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
type PatVarLabel (Arg b) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
type ConOfAbs (Arg a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type AbsOfCon (Arg c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
type ReifiesTo (Arg i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type AbsOfRef (Arg r) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |||||
type AbsOfRef [Arg r] Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |||||
type SubstArg (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Substitute |
A function argument can be hidden and/or irrelevant.
ArgInfo | |
|
Instances
LensAnnotation ArgInfo Source # | |
Defined in Agda.Syntax.Common getAnnotation :: ArgInfo -> Annotation Source # setAnnotation :: Annotation -> ArgInfo -> ArgInfo Source # mapAnnotation :: (Annotation -> Annotation) -> ArgInfo -> ArgInfo Source # | |
LensArgInfo ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensCohesion ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensFreeVariables ArgInfo Source # | |
Defined in Agda.Syntax.Common getFreeVariables :: ArgInfo -> FreeVariables Source # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo Source # | |
LensHiding ArgInfo Source # | |
LensLock ArgInfo Source # | |
LensModality ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensOrigin ArgInfo Source # | |
LensQuantity ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
HasRange ArgInfo Source # | |
KillRange ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
EqualSy ArgInfo Source # | Ignore origin and free variables. |
ToTerm ArgInfo Source # | |
ChooseFlex ArgInfo Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: ArgInfo -> ArgInfo -> FlexChoice Source # | |
EmbPrj ArgInfo Source # | |
SynEq ArgInfo Source # | |
Unquote ArgInfo Source # | |
NFData ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
Show ArgInfo Source # | |
Eq ArgInfo Source # | |
Ord ArgInfo Source # | |
Where does the ConP
or Con
come from?
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. |
Instances
KillRange ConOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
EmbPrj ConOrigin Source # | |||||
NFData ConOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
Bounded ConOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum ConOrigin Source # | |||||
Generic ConOrigin Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show ConOrigin Source # | |||||
Eq ConOrigin Source # | |||||
Ord ConOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
type Rep ConOrigin Source # | |||||
Defined in Agda.Syntax.Common type Rep ConOrigin = D1 ('MetaData "ConOrigin" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "ConOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ConORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOSplit" 'PrefixI 'False) (U1 :: Type -> Type))) |
Instances
LensHiding Hiding Source # | |
Pretty Hiding Source # | |
HasRange Hiding Source # | |
KillRange Hiding Source # | |
Defined in Agda.Syntax.Common | |
Verbalize Hiding Source # | |
Defined in Agda.TypeChecking.Errors | |
ChooseFlex Hiding Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: Hiding -> Hiding -> FlexChoice Source # | |
EmbPrj Hiding Source # | |
Unquote Hiding Source # | |
Null Hiding Source # | |
NFData Hiding Source # | |
Defined in Agda.Syntax.Common | |
Monoid Hiding Source # | |
Semigroup Hiding Source # |
|
Show Hiding Source # | |
Eq Hiding Source # | |
Ord Hiding Source # | |
class LensOrigin a where Source #
A lens to access the Origin
attribute in data structures.
Minimal implementation: getOrigin
and mapOrigin
or LensArgInfo
.
Nothing
getOrigin :: a -> Origin Source #
default getOrigin :: LensArgInfo a => a -> Origin Source #
Instances
LensOrigin ArgInfo Source # | |
LensOrigin Origin Source # | |
LensOrigin AppInfo Source # | |
LensOrigin (Arg e) Source # | |
LensOrigin (WithOrigin a) Source # | |
Defined in Agda.Syntax.Common getOrigin :: WithOrigin a -> Origin Source # setOrigin :: Origin -> WithOrigin a -> WithOrigin a Source # mapOrigin :: (Origin -> Origin) -> WithOrigin a -> WithOrigin a Source # | |
LensOrigin (Elim' a) Source # | This instance cheats on |
LensOrigin (FlexibleVar a) Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem getOrigin :: FlexibleVar a -> Origin Source # setOrigin :: Origin -> FlexibleVar a -> FlexibleVar a Source # mapOrigin :: (Origin -> Origin) -> FlexibleVar a -> FlexibleVar a Source # | |
LensOrigin (Dom' t e) Source # | |
The unique identifier of a name. Second argument is the top-level module identifier.
NameId !Word64 !ModuleNameHash |
Instances
Pretty NameId Source # | |||||
KillRange NameId Source # | |||||
Defined in Agda.Syntax.Common | |||||
HasFresh NameId Source # | |||||
EmbPrj NameId Source # | |||||
NFData NameId Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum NameId Source # | |||||
Generic NameId Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show NameId Source # | |||||
Eq NameId Source # | |||||
Ord NameId Source # | |||||
Hashable NameId Source # | |||||
Defined in Agda.Syntax.Common hashWithSalt :: Int -> NameId -> Int | |||||
MonadFresh NameId AbsToCon Source # | |||||
Monad m => MonadFresh NameId (PureConversionT m) Source # | |||||
Defined in Agda.TypeChecking.Conversion.Pure fresh :: PureConversionT m NameId Source # | |||||
type Rep NameId Source # | |||||
Defined in Agda.Syntax.Common type Rep NameId = D1 ('MetaData "NameId" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "NameId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash))) |
Something potentially carrying a name.
Named | |
|
Instances
MapNamedArgPattern NAP Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
PatternLike a b => PatternLike a (Named x b) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
Pretty e => Pretty (Named_ e) Source # | |||||
PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal
patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source # | |||||
PrettyTCM (NamedArg Expr) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (NamedArg Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Named_ Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
NormaliseProjP a => NormaliseProjP (Named_ a) Source # | |||||
Defined in Agda.TypeChecking.Records normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source # | |||||
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
DeBruijn a => DeBruijn (Named_ a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn deBruijnVar :: Int -> Named_ a Source # debruijnNamedVar :: String -> Int -> Named_ a Source # deBruijnView :: Named_ a -> Maybe Int Source # | |||||
IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path iApplyVars :: NamedArg p -> [Int] Source # | |||||
Decoration (Named name) Source # | |||||
Functor (Named name) Source # | |||||
Foldable (Named name) Source # | |||||
Defined in Agda.Syntax.Common fold :: Monoid m => Named name m -> m foldMap :: Monoid m => (a -> m) -> Named name a -> m foldMap' :: Monoid m => (a -> m) -> Named name a -> m foldr :: (a -> b -> b) -> b -> Named name a -> b foldr' :: (a -> b -> b) -> b -> Named name a -> b foldl :: (b -> a -> b) -> b -> Named name a -> b foldl' :: (b -> a -> b) -> b -> Named name a -> b foldr1 :: (a -> a -> a) -> Named name a -> a foldl1 :: (a -> a -> a) -> Named name a -> a elem :: Eq a => a -> Named name a -> Bool maximum :: Ord a => Named name a -> a minimum :: Ord a => Named name a -> a | |||||
Traversable (Named name) Source # | |||||
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
SubstExpr a => SubstExpr (Named name a) Source # | |||||
IsProjP a => IsProjP (Named n a) Source # | |||||
Defined in Agda.Syntax.Abstract.Name isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |||||
APatternLike a => APatternLike (Named n a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern foldrAPattern :: Monoid m => (Pattern' (ADotT (Named n a)) -> m -> m) -> Named n a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (Named n a)) -> m (Pattern' (ADotT (Named n a)))) -> (Pattern' (ADotT (Named n a)) -> m (Pattern' (ADotT (Named n a)))) -> Named n a -> m (Named n a) Source # | |||||
DeclaredNames a => DeclaredNames (Named name a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views declaredNames :: Collection KName m => Named name a -> m Source # | |||||
ExprLike a => ExprLike (Named x a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m (Named x a) Source # foldExpr :: FoldExprFn m (Named x a) Source # traverseExpr :: TraverseExprFn m (Named x a) Source # mapExpr :: (Expr -> Expr) -> Named x a -> Named x a Source # | |||||
LensHiding a => LensHiding (Named nm a) Source # | |||||
LensNamed (Named name a) Source # | |||||
ExprLike a => ExprLike (Named name a) Source # | |||||
CPatternLike p => CPatternLike (Named n p) Source # | |||||
Defined in Agda.Syntax.Concrete.Pattern foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Named n p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Named n p -> m (Named n p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Named n p -> m (Named n p) Source # | |||||
IsWithP p => IsWithP (Named n p) Source # | |||||
NamesIn a => NamesIn (Named n a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
CountPatternVars a => CountPatternVars (Named x a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern countPatternVars :: Named x a -> Int Source # | |||||
PatternVarModalities a => PatternVarModalities (Named s a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
HasRange a => HasRange (Named name a) Source # | |||||
(KillRange name, KillRange a) => KillRange (Named name a) Source # | |||||
Defined in Agda.Syntax.Common killRange :: KillRangeT (Named name a) Source # | |||||
SetRange a => SetRange (Named name a) Source # | |||||
ToConcrete a => ToConcrete (Named name a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
| |||||
ToAbstract c => ToAbstract (Named name c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
| |||||
Reify i => Reify (Named n i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract
| |||||
ToAbstract r => ToAbstract (Named name r) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract
toAbstract :: MonadReflectedToAbstract m => Named name r -> m (AbsOfRef (Named name r)) Source # | |||||
Free t => Free (Named nm t) Source # | |||||
AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Abstract | |||||
InstantiateFull t => InstantiateFull (Named name t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise t => Normalise (Named name t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Simplify t => Simplify (Named name t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
IsFlexiblePattern a => IsFlexiblePattern (Named name a) Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Named name a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Named name a -> m Bool Source # | |||||
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source # | |||||
Subst a => Subst (Named name a) Source # | |||||
Defined in Agda.TypeChecking.Substitute
applySubst :: Substitution' (SubstArg (Named name a)) -> Named name a -> Named name a Source # | |||||
PiApplyM a => PiApplyM (Named n a) Source # | |||||
Defined in Agda.TypeChecking.Telescope piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Named n a -> m Type Source # piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Named n a -> m Type Source # | |||||
(NFData name, NFData a) => NFData (Named name a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
(Show name, Show a) => Show (Named name a) Source # | |||||
(Eq name, Eq a) => Eq (Named name a) Source # | |||||
(Ord name, Ord a) => Ord (Named name a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
PatternToExpr p e => PatternToExpr (Named n p) (Named n e) Source # | |||||
LabelPatVars a b => LabelPatVars (Named x a) (Named x b) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern
labelPatVars :: Named x a -> State [PatVarLabel (Named x b)] (Named x b) Source # unlabelPatVars :: Named x b -> Named x a Source # | |||||
TermToPattern a b => TermToPattern (Named c a) (Named c b) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Internal | |||||
type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type ADotT (Named n a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
type NameOf (Named name a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
type PatVar (Named s a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
type PatVarLabel (Named x b) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
type ConOfAbs (Named name a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type AbsOfCon (Named name c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
type ReifiesTo (Named n i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type AbsOfRef (Named name r) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |||||
type SubstArg (Named name a) Source # | |||||
Defined in Agda.TypeChecking.Substitute |
class LensHiding a where Source #
A lens to access the Hiding
attribute in data structures.
Minimal implementation: getHiding
and mapHiding
or LensArgInfo
.
Nothing
getHiding :: a -> Hiding Source #
default getHiding :: LensArgInfo a => a -> Hiding Source #
Instances
LensHiding LamBinding Source # | |
Defined in Agda.Syntax.Abstract getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |
LensHiding TypedBinding Source # | |
Defined in Agda.Syntax.Abstract getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source # | |
LensHiding ArgInfo Source # | |
LensHiding Hiding Source # | |
LensHiding LamBinding Source # | |
Defined in Agda.Syntax.Concrete getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |
LensHiding TypedBinding Source # | |
Defined in Agda.Syntax.Concrete getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source # | |
LensHiding (Arg e) Source # | |
LensHiding (WithHiding a) Source # | |
Defined in Agda.Syntax.Common getHiding :: WithHiding a -> Hiding Source # setHiding :: Hiding -> WithHiding a -> WithHiding a Source # mapHiding :: (Hiding -> Hiding) -> WithHiding a -> WithHiding a Source # | |
LensHiding (FlexibleVar a) Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem getHiding :: FlexibleVar a -> Hiding Source # setHiding :: Hiding -> FlexibleVar a -> FlexibleVar a Source # mapHiding :: (Hiding -> Hiding) -> FlexibleVar a -> FlexibleVar a Source # | |
LensHiding a => LensHiding (Named nm a) Source # | |
LensHiding (Dom' t e) Source # | |
data ProjOrigin Source #
Where does a projection come from?
ProjPrefix | User wrote a prefix projection. |
ProjPostfix | User wrote a postfix projection. |
ProjSystem | Projection was generated by the system. |
Instances
KillRange ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
EmbPrj ProjOrigin Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: ProjOrigin -> S Int32 Source # icod_ :: ProjOrigin -> S Int32 Source # value :: Int32 -> R ProjOrigin Source # | |||||
NFData ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common rnf :: ProjOrigin -> () | |||||
Bounded ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common succ :: ProjOrigin -> ProjOrigin pred :: ProjOrigin -> ProjOrigin toEnum :: Int -> ProjOrigin fromEnum :: ProjOrigin -> Int enumFrom :: ProjOrigin -> [ProjOrigin] enumFromThen :: ProjOrigin -> ProjOrigin -> [ProjOrigin] enumFromTo :: ProjOrigin -> ProjOrigin -> [ProjOrigin] enumFromThenTo :: ProjOrigin -> ProjOrigin -> ProjOrigin -> [ProjOrigin] | |||||
Generic ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common
from :: ProjOrigin -> Rep ProjOrigin x to :: Rep ProjOrigin x -> ProjOrigin | |||||
Show ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> ProjOrigin -> ShowS show :: ProjOrigin -> String showList :: [ProjOrigin] -> ShowS | |||||
Eq ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common (==) :: ProjOrigin -> ProjOrigin -> Bool (/=) :: ProjOrigin -> ProjOrigin -> Bool | |||||
Ord ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common compare :: ProjOrigin -> ProjOrigin -> Ordering (<) :: ProjOrigin -> ProjOrigin -> Bool (<=) :: ProjOrigin -> ProjOrigin -> Bool (>) :: ProjOrigin -> ProjOrigin -> Bool (>=) :: ProjOrigin -> ProjOrigin -> Bool max :: ProjOrigin -> ProjOrigin -> ProjOrigin min :: ProjOrigin -> ProjOrigin -> ProjOrigin | |||||
type Rep ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common type Rep ProjOrigin = D1 ('MetaData "ProjOrigin" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ProjPrefix" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ProjPostfix" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProjSystem" 'PrefixI 'False) (U1 :: Type -> Type))) |
data WithOrigin a Source #
Decorating something with Origin
information.
Instances
MapNamedArgPattern NAP Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
Decoration WithOrigin Source # | |||||
Defined in Agda.Syntax.Common traverseF :: Functor m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) Source # distributeF :: Functor m => WithOrigin (m a) -> m (WithOrigin a) Source # | |||||
Functor WithOrigin Source # | |||||
Defined in Agda.Syntax.Common fmap :: (a -> b) -> WithOrigin a -> WithOrigin b (<$) :: a -> WithOrigin b -> WithOrigin a # | |||||
Foldable WithOrigin Source # | |||||
Defined in Agda.Syntax.Common fold :: Monoid m => WithOrigin m -> m foldMap :: Monoid m => (a -> m) -> WithOrigin a -> m foldMap' :: Monoid m => (a -> m) -> WithOrigin a -> m foldr :: (a -> b -> b) -> b -> WithOrigin a -> b foldr' :: (a -> b -> b) -> b -> WithOrigin a -> b foldl :: (b -> a -> b) -> b -> WithOrigin a -> b foldl' :: (b -> a -> b) -> b -> WithOrigin a -> b foldr1 :: (a -> a -> a) -> WithOrigin a -> a foldl1 :: (a -> a -> a) -> WithOrigin a -> a toList :: WithOrigin a -> [a] null :: WithOrigin a -> Bool length :: WithOrigin a -> Int elem :: Eq a => a -> WithOrigin a -> Bool maximum :: Ord a => WithOrigin a -> a minimum :: Ord a => WithOrigin a -> a sum :: Num a => WithOrigin a -> a product :: Num a => WithOrigin a -> a | |||||
Traversable WithOrigin Source # | |||||
Defined in Agda.Syntax.Common traverse :: Applicative f => (a -> f b) -> WithOrigin a -> f (WithOrigin b) sequenceA :: Applicative f => WithOrigin (f a) -> f (WithOrigin a) mapM :: Monad m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) sequence :: Monad m => WithOrigin (m a) -> m (WithOrigin a) | |||||
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
LensOrigin (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common getOrigin :: WithOrigin a -> Origin Source # setOrigin :: Origin -> WithOrigin a -> WithOrigin a Source # mapOrigin :: (Origin -> Origin) -> WithOrigin a -> WithOrigin a Source # | |||||
Pretty e => Pretty (Named_ e) Source # | |||||
Pretty a => Pretty (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common pretty :: WithOrigin a -> Doc Source # prettyPrec :: Int -> WithOrigin a -> Doc Source # prettyList :: [WithOrigin a] -> Doc Source # | |||||
IsNoName a => IsNoName (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Concrete.Name isNoName :: WithOrigin a -> Bool Source # | |||||
PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal
patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source # | |||||
HasRange a => HasRange (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common getRange :: WithOrigin a -> Range Source # | |||||
KillRange a => KillRange (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common killRange :: KillRangeT (WithOrigin a) Source # | |||||
SetRange a => SetRange (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common setRange :: Range -> WithOrigin a -> WithOrigin a Source # | |||||
PrettyTCM (NamedArg Expr) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (NamedArg Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Named_ Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
NormaliseProjP a => NormaliseProjP (Named_ a) Source # | |||||
Defined in Agda.TypeChecking.Records normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source # | |||||
EmbPrj a => EmbPrj (WithOrigin a) Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: WithOrigin a -> S Int32 Source # icod_ :: WithOrigin a -> S Int32 Source # value :: Int32 -> R (WithOrigin a) Source # | |||||
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
DeBruijn a => DeBruijn (Named_ a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn deBruijnVar :: Int -> Named_ a Source # debruijnNamedVar :: String -> Int -> Named_ a Source # deBruijnView :: Named_ a -> Maybe Int Source # | |||||
IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path iApplyVars :: NamedArg p -> [Int] Source # | |||||
NFData a => NFData (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common rnf :: WithOrigin a -> () | |||||
Show a => Show (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> WithOrigin a -> ShowS show :: WithOrigin a -> String showList :: [WithOrigin a] -> ShowS | |||||
Eq a => Eq (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common (==) :: WithOrigin a -> WithOrigin a -> Bool (/=) :: WithOrigin a -> WithOrigin a -> Bool | |||||
Ord a => Ord (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common compare :: WithOrigin a -> WithOrigin a -> Ordering (<) :: WithOrigin a -> WithOrigin a -> Bool (<=) :: WithOrigin a -> WithOrigin a -> Bool (>) :: WithOrigin a -> WithOrigin a -> Bool (>=) :: WithOrigin a -> WithOrigin a -> Bool max :: WithOrigin a -> WithOrigin a -> WithOrigin a min :: WithOrigin a -> WithOrigin a -> WithOrigin a | |||||
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal |
visible :: LensHiding a => a -> Bool Source #
NotHidden
arguments are visible
.
data TerminationCheck m Source #
Termination check? (Default = TerminationCheck).
TerminationCheck | Run the termination checker. |
NoTerminationCheck | Skip termination checking (unsafe). |
NonTerminating | Treat as non-terminating. |
Terminating | Treat as terminating (unsafe). Same effect as |
TerminationMeasure Range m | Skip termination checking but use measure instead. |
Instances
Functor TerminationCheck Source # | |
Defined in Agda.Syntax.Common fmap :: (a -> b) -> TerminationCheck a -> TerminationCheck b (<$) :: a -> TerminationCheck b -> TerminationCheck a # | |
KillRange m => KillRange (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common killRange :: KillRangeT (TerminationCheck m) Source # | |
NFData a => NFData (TerminationCheck a) Source # | |
Defined in Agda.Syntax.Common rnf :: TerminationCheck a -> () | |
Show m => Show (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> TerminationCheck m -> ShowS show :: TerminationCheck m -> String showList :: [TerminationCheck m] -> ShowS | |
Eq m => Eq (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common (==) :: TerminationCheck m -> TerminationCheck m -> Bool (/=) :: TerminationCheck m -> TerminationCheck m -> Bool |
type Notation = [NotationPart] Source #
Notation as provided by the syntax
declaration.
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.
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. |
Instances
LensCohesion Cohesion Source # | |||||
Defined in Agda.Syntax.Common | |||||
Pretty Cohesion Source # | |||||
HasRange Cohesion Source # | |||||
KillRange Cohesion Source # | |||||
Defined in Agda.Syntax.Common | |||||
SetRange Cohesion Source # | |||||
Verbalize Cohesion Source # | |||||
Defined in Agda.TypeChecking.Errors | |||||
EmbPrj Cohesion Source # | |||||
PartialOrd Cohesion Source # | Flatter is smaller. | ||||
Defined in Agda.Syntax.Common | |||||
NFData Cohesion Source # | |||||
Defined in Agda.Syntax.Common | |||||
Bounded Cohesion Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum Cohesion Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic Cohesion Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show Cohesion Source # | |||||
Eq Cohesion Source # | |||||
Ord Cohesion Source # | Order is given by implication: flatter is smaller. | ||||
LeftClosedPOMonoid (UnderComposition Cohesion) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POMonoid (UnderAddition Cohesion) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POMonoid (UnderComposition Cohesion) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POSemigroup (UnderAddition Cohesion) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POSemigroup (UnderComposition Cohesion) Source # | |||||
Defined in Agda.Syntax.Common | |||||
Monoid (UnderAddition Cohesion) Source # |
| ||||
Defined in Agda.Syntax.Common | |||||
Monoid (UnderComposition Cohesion) Source # |
| ||||
Semigroup (UnderAddition Cohesion) Source # |
| ||||
Defined in Agda.Syntax.Common (<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion # sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion | |||||
Semigroup (UnderComposition Cohesion) Source # |
| ||||
Defined in Agda.Syntax.Common (<>) :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion # sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion | |||||
type Rep Cohesion Source # | |||||
Defined in Agda.Syntax.Common type Rep Cohesion = D1 ('MetaData "Cohesion" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Flat" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Continuous" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Squash" 'PrefixI 'False) (U1 :: Type -> Type))) |
data RecordDirectives' a Source #
RecordDirectives | |
|
Instances
DeclaredNames RecordDirectives Source # | |||||
Defined in Agda.Syntax.Abstract.Views declaredNames :: Collection KName m => RecordDirectives -> m Source # | |||||
ToConcrete RecordDirectives Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: RecordDirectives -> AbsToCon (ConOfAbs RecordDirectives) Source # bindToConcrete :: RecordDirectives -> (ConOfAbs RecordDirectives -> AbsToCon b) -> AbsToCon b Source # | |||||
Functor RecordDirectives' Source # | |||||
Defined in Agda.Syntax.Common fmap :: (a -> b) -> RecordDirectives' a -> RecordDirectives' b (<$) :: a -> RecordDirectives' b -> RecordDirectives' a # | |||||
Foldable RecordDirectives' Source # | |||||
Defined in Agda.Syntax.Common fold :: Monoid m => RecordDirectives' m -> m foldMap :: Monoid m => (a -> m) -> RecordDirectives' a -> m foldMap' :: Monoid m => (a -> m) -> RecordDirectives' a -> m foldr :: (a -> b -> b) -> b -> RecordDirectives' a -> b foldr' :: (a -> b -> b) -> b -> RecordDirectives' a -> b foldl :: (b -> a -> b) -> b -> RecordDirectives' a -> b foldl' :: (b -> a -> b) -> b -> RecordDirectives' a -> b foldr1 :: (a -> a -> a) -> RecordDirectives' a -> a foldl1 :: (a -> a -> a) -> RecordDirectives' a -> a toList :: RecordDirectives' a -> [a] null :: RecordDirectives' a -> Bool length :: RecordDirectives' a -> Int elem :: Eq a => a -> RecordDirectives' a -> Bool maximum :: Ord a => RecordDirectives' a -> a minimum :: Ord a => RecordDirectives' a -> a sum :: Num a => RecordDirectives' a -> a product :: Num a => RecordDirectives' a -> a | |||||
Traversable RecordDirectives' Source # | |||||
Defined in Agda.Syntax.Common traverse :: Applicative f => (a -> f b) -> RecordDirectives' a -> f (RecordDirectives' b) sequenceA :: Applicative f => RecordDirectives' (f a) -> f (RecordDirectives' a) mapM :: Monad m => (a -> m b) -> RecordDirectives' a -> m (RecordDirectives' b) sequence :: Monad m => RecordDirectives' (m a) -> m (RecordDirectives' a) | |||||
HasRange a => HasRange (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common getRange :: RecordDirectives' a -> Range Source # | |||||
KillRange a => KillRange (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common killRange :: KillRangeT (RecordDirectives' a) Source # | |||||
EmbPrj a => EmbPrj (RecordDirectives' a) Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: RecordDirectives' a -> S Int32 Source # icod_ :: RecordDirectives' a -> S Int32 Source # value :: Int32 -> R (RecordDirectives' a) Source # | |||||
Null (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common empty :: RecordDirectives' a Source # null :: RecordDirectives' a -> Bool Source # | |||||
NFData a => NFData (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common rnf :: RecordDirectives' a -> () | |||||
Show a => Show (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> RecordDirectives' a -> ShowS show :: RecordDirectives' a -> String showList :: [RecordDirectives' a] -> ShowS | |||||
Eq a => Eq (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common (==) :: RecordDirectives' a -> RecordDirectives' a -> Bool (/=) :: RecordDirectives' a -> RecordDirectives' a -> Bool | |||||
type ConOfAbs RecordDirectives Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete |
The using
clause of import directive.
UseEverything | No |
Using [ImportedName' n m] |
|
Instances
(Pretty a, Pretty b) => Pretty (Using' a b) Source # | |
(HasRange a, HasRange b) => HasRange (Using' a b) Source # | |
(KillRange a, KillRange b) => KillRange (Using' a b) Source # | |
Defined in Agda.Syntax.Common killRange :: KillRangeT (Using' a b) Source # | |
Null (Using' n m) Source # | |
(NFData a, NFData b) => NFData (Using' a b) Source # | |
Defined in Agda.Syntax.Common | |
Monoid (Using' n m) Source # | |
Semigroup (Using' n m) Source # | |
(Show a, Show b) => Show (Using' a b) | |
(Eq m, Eq n) => Eq (Using' n m) Source # | |
data ImportedName' n m Source #
An imported name can be a module or a defined name.
ImportedModule m | Imported module name of type |
ImportedName n | Imported name of type |
Instances
(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Concrete.Pretty pretty :: ImportedName' a b -> Doc Source # prettyPrec :: Int -> ImportedName' a b -> Doc Source # prettyList :: [ImportedName' a b] -> Doc Source # | |
(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common getRange :: ImportedName' a b -> Range Source # | |
(KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common killRange :: KillRangeT (ImportedName' a b) Source # | |
(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: ImportedName' a b -> S Int32 Source # icod_ :: ImportedName' a b -> S Int32 Source # value :: Int32 -> R (ImportedName' a b) Source # | |
(NFData a, NFData b) => NFData (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common rnf :: ImportedName' a b -> () | |
(Show m, Show n) => Show (ImportedName' n m) Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> ImportedName' n m -> ShowS show :: ImportedName' n m -> String showList :: [ImportedName' n m] -> ShowS | |
(Eq m, Eq n) => Eq (ImportedName' n m) Source # | |
Defined in Agda.Syntax.Common (==) :: ImportedName' n m -> ImportedName' n m -> Bool (/=) :: ImportedName' n m -> ImportedName' n m -> Bool | |
(Ord m, Ord n) => Ord (ImportedName' n m) Source # | |
Defined in Agda.Syntax.Common compare :: ImportedName' n m -> ImportedName' n m -> Ordering (<) :: ImportedName' n m -> ImportedName' n m -> Bool (<=) :: ImportedName' n m -> ImportedName' n m -> Bool (>) :: ImportedName' n m -> ImportedName' n m -> Bool (>=) :: ImportedName' n m -> ImportedName' n m -> Bool max :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m min :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m |
Renaming | |
|
Instances
(Pretty a, Pretty b) => Pretty (Renaming' a b) Source # | |
(HasRange a, HasRange b) => HasRange (Renaming' a b) Source # | |
(KillRange a, KillRange b) => KillRange (Renaming' a b) Source # | |
Defined in Agda.Syntax.Common killRange :: KillRangeT (Renaming' a b) Source # | |
(NFData a, NFData b) => NFData (Renaming' a b) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common | |
(Show a, Show b) => Show (Renaming' a b) | |
(Eq m, Eq n) => Eq (Renaming' n m) Source # | |
IsNotLock | |
IsLock LockOrigin | In the future there might be different kinds of them. For now we assume lock weakening. |
Instances
LensLock Lock Source # | |||||
Pretty Lock Source # | |||||
EmbPrj Lock Source # | |||||
NFData Lock Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic Lock Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show Lock Source # | |||||
Eq Lock Source # | |||||
Ord Lock Source # | |||||
type Rep Lock Source # | |||||
Defined in Agda.Syntax.Common type Rep Lock = D1 ('MetaData "Lock" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "IsNotLock" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsLock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LockOrigin))) |
Variants of Cubical Agda.
Instances
EmbPrj Cubical Source # | |||||
NFData Cubical Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic Cubical Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show Cubical Source # | |||||
Eq Cubical Source # | |||||
type Rep Cubical Source # | |||||
Defined in Agda.Syntax.Common type Rep Cubical = D1 ('MetaData "Cubical" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "CErased" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CFull" 'PrefixI 'False) (U1 :: Type -> Type)) |
Agda variants.
Only some variants are tracked.
Instances
KillRange Language Source # | |||||
Defined in Agda.Syntax.Common | |||||
EmbPrj Language Source # | |||||
NFData Language Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic Language Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show Language Source # | |||||
Eq Language Source # | |||||
type Rep Language Source # | |||||
Defined in Agda.Syntax.Common type Rep Language = D1 ('MetaData "Language" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "WithoutK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cubical" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cubical)))) |
Opaque or transparent.
OpaqueDef !OpaqueId | This definition is opaque, and it is guarded by the given opaque block. |
TransparentDef |
Instances
AllAreOpaque IsOpaque Source # | |||||
Defined in Agda.Syntax.Common jointOpacity :: IsOpaque -> JointOpacity Source # | |||||
LensIsOpaque IsOpaque Source # | |||||
Defined in Agda.Syntax.Common | |||||
KillRange IsOpaque Source # | |||||
Defined in Agda.Syntax.Common | |||||
EmbPrj IsOpaque Source # | |||||
NFData IsOpaque Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic IsOpaque Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show IsOpaque Source # | |||||
Eq IsOpaque Source # | |||||
Ord IsOpaque Source # | |||||
type Rep IsOpaque Source # | |||||
Defined in Agda.Syntax.Common type Rep IsOpaque = D1 ('MetaData "IsOpaque" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "OpaqueDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 OpaqueId)) :+: C1 ('MetaCons "TransparentDef" 'PrefixI 'False) (U1 :: Type -> Type)) |
fromImportedName :: ImportedName' a a -> a Source #
partitionImportedNames :: [ImportedName' n m] -> ([n], [m]) Source #
Like partitionEithers
.
defaultArg :: a -> Arg a Source #
A function argument can be relevant or irrelevant. See Agda.TypeChecking.Irrelevance.
Relevant | The argument is (possibly) relevant at compile-time. |
NonStrict | The argument may never flow into evaluation position. Therefore, it is irrelevant at run-time. It is treated relevantly during equality checking. The above comment is probably obsolete, as we currently have
erasure (at0, |
Irrelevant | The argument is irrelevant at compile- and runtime. |
Instances
LensRelevance Relevance Source # | |||||
Defined in Agda.Syntax.Common | |||||
Pretty Relevance Source # | |||||
HasRange Relevance Source # | |||||
KillRange Relevance Source # | |||||
Defined in Agda.Syntax.Common | |||||
SetRange Relevance Source # | |||||
Verbalize Relevance Source # | |||||
Defined in Agda.TypeChecking.Errors | |||||
PrettyTCM Relevance Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
EmbPrj Relevance Source # | |||||
Unquote Relevance Source # | |||||
PartialOrd Relevance Source # | More relevant is smaller. | ||||
Defined in Agda.Syntax.Common | |||||
NFData Relevance Source # | |||||
Defined in Agda.Syntax.Common | |||||
Bounded Relevance Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum Relevance Source # | |||||
Generic Relevance Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show Relevance Source # | |||||
Eq Relevance Source # | |||||
Ord Relevance Source # | More relevant is smaller. | ||||
Defined in Agda.Syntax.Common | |||||
LeftClosedPOMonoid (UnderComposition Relevance) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POMonoid (UnderAddition Relevance) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POMonoid (UnderComposition Relevance) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POSemigroup (UnderAddition Relevance) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POSemigroup (UnderComposition Relevance) Source # | |||||
Defined in Agda.Syntax.Common | |||||
Monoid (UnderAddition Relevance) Source # | |||||
Defined in Agda.Syntax.Common | |||||
Monoid (UnderComposition Relevance) Source # |
| ||||
Semigroup (UnderAddition Relevance) Source # | |||||
Defined in Agda.Syntax.Common (<>) :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance # sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance | |||||
Semigroup (UnderComposition Relevance) Source # |
| ||||
Defined in Agda.Syntax.Common (<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance # sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance | |||||
type Rep Relevance Source # | |||||
Defined in Agda.Syntax.Common type Rep Relevance = D1 ('MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Relevant" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonStrict" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Irrelevant" 'PrefixI 'False) (U1 :: Type -> Type))) |
class LensRelevance a where Source #
A lens to access the Relevance
attribute in data structures.
Minimal implementation: getRelevance
and mapRelevance
or LensModality
.
Nothing
getRelevance :: a -> Relevance Source #
default getRelevance :: LensModality a => a -> Relevance Source #
setRelevance :: Relevance -> a -> a Source #
mapRelevance :: (Relevance -> Relevance) -> a -> a Source #
default mapRelevance :: LensModality a => (Relevance -> Relevance) -> a -> a Source #
Instances
LensRelevance ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance Modality Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance Relevance Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance TypedBinding Source # | |
Defined in Agda.Syntax.Concrete getRelevance :: TypedBinding -> Relevance Source # setRelevance :: Relevance -> TypedBinding -> TypedBinding Source # mapRelevance :: (Relevance -> Relevance) -> TypedBinding -> TypedBinding Source # | |
LensRelevance Definition Source # | |
Defined in Agda.TypeChecking.Monad.Base getRelevance :: Definition -> Relevance Source # setRelevance :: Relevance -> Definition -> Definition Source # mapRelevance :: (Relevance -> Relevance) -> Definition -> Definition Source # | |
LensRelevance MetaInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
LensRelevance MetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base getRelevance :: MetaVariable -> Relevance Source # setRelevance :: Relevance -> MetaVariable -> MetaVariable Source # mapRelevance :: (Relevance -> Relevance) -> MetaVariable -> MetaVariable Source # | |
LensRelevance RemoteMetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
LensRelevance (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
LensRelevance (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal | |
LensRelevance (FreeEnv' a b c) Source # | |
Defined in Agda.TypeChecking.Free.Lazy |
hasQuantity0 :: LensQuantity a => a -> Bool Source #
Check for Quantity0
.
data WithHiding a Source #
Decorating something with Hiding
information.
Instances
Decoration WithHiding Source # | |||||
Defined in Agda.Syntax.Common traverseF :: Functor m => (a -> m b) -> WithHiding a -> m (WithHiding b) Source # distributeF :: Functor m => WithHiding (m a) -> m (WithHiding a) Source # | |||||
Applicative WithHiding Source # | |||||
Defined in Agda.Syntax.Common pure :: a -> WithHiding a (<*>) :: WithHiding (a -> b) -> WithHiding a -> WithHiding b # liftA2 :: (a -> b -> c) -> WithHiding a -> WithHiding b -> WithHiding c (*>) :: WithHiding a -> WithHiding b -> WithHiding b (<*) :: WithHiding a -> WithHiding b -> WithHiding a | |||||
Functor WithHiding Source # | |||||
Defined in Agda.Syntax.Common fmap :: (a -> b) -> WithHiding a -> WithHiding b (<$) :: a -> WithHiding b -> WithHiding a # | |||||
Foldable WithHiding Source # | |||||
Defined in Agda.Syntax.Common fold :: Monoid m => WithHiding m -> m foldMap :: Monoid m => (a -> m) -> WithHiding a -> m foldMap' :: Monoid m => (a -> m) -> WithHiding a -> m foldr :: (a -> b -> b) -> b -> WithHiding a -> b foldr' :: (a -> b -> b) -> b -> WithHiding a -> b foldl :: (b -> a -> b) -> b -> WithHiding a -> b foldl' :: (b -> a -> b) -> b -> WithHiding a -> b foldr1 :: (a -> a -> a) -> WithHiding a -> a foldl1 :: (a -> a -> a) -> WithHiding a -> a toList :: WithHiding a -> [a] null :: WithHiding a -> Bool length :: WithHiding a -> Int elem :: Eq a => a -> WithHiding a -> Bool maximum :: Ord a => WithHiding a -> a minimum :: Ord a => WithHiding a -> a sum :: Num a => WithHiding a -> a product :: Num a => WithHiding a -> a | |||||
Traversable WithHiding Source # | |||||
Defined in Agda.Syntax.Common traverse :: Applicative f => (a -> f b) -> WithHiding a -> f (WithHiding b) sequenceA :: Applicative f => WithHiding (f a) -> f (WithHiding a) mapM :: Monad m => (a -> m b) -> WithHiding a -> m (WithHiding b) sequence :: Monad m => WithHiding (m a) -> m (WithHiding a) | |||||
ExprLike a => ExprLike (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views recurseExpr :: RecurseExprFn m (WithHiding a) Source # foldExpr :: FoldExprFn m (WithHiding a) Source # traverseExpr :: TraverseExprFn m (WithHiding a) Source # mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a Source # | |||||
LensHiding (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common getHiding :: WithHiding a -> Hiding Source # setHiding :: Hiding -> WithHiding a -> WithHiding a Source # mapHiding :: (Hiding -> Hiding) -> WithHiding a -> WithHiding a Source # | |||||
Pretty a => Pretty (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Concrete.Pretty pretty :: WithHiding a -> Doc Source # prettyPrec :: Int -> WithHiding a -> Doc Source # prettyList :: [WithHiding a] -> Doc Source # | |||||
ExprLike a => ExprLike (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Concrete.Generic mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a Source # foldExpr :: Monoid m => (Expr -> m) -> WithHiding a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WithHiding a -> m (WithHiding a) Source # | |||||
TermLike a => TermLike (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Internal.Generic traverseTermM :: Monad m => (Term -> m Term) -> WithHiding a -> m (WithHiding a) Source # foldTerm :: Monoid m => (Term -> m) -> WithHiding a -> m Source # | |||||
HasRange a => HasRange (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common getRange :: WithHiding a -> Range Source # | |||||
KillRange a => KillRange (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common killRange :: KillRangeT (WithHiding a) Source # | |||||
SetRange a => SetRange (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common setRange :: Range -> WithHiding a -> WithHiding a Source # | |||||
ToConcrete a => ToConcrete (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: WithHiding a -> AbsToCon (ConOfAbs (WithHiding a)) Source # bindToConcrete :: WithHiding a -> (ConOfAbs (WithHiding a) -> AbsToCon b) -> AbsToCon b Source # | |||||
ToAbstract c => ToAbstract (WithHiding c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract
toAbstract :: WithHiding c -> ScopeM (AbsOfCon (WithHiding c)) Source # | |||||
Free t => Free (WithHiding t) Source # | |||||
Defined in Agda.TypeChecking.Free.Lazy | |||||
PrettyTCM a => PrettyTCM (WithHiding a) Source # | |||||
Defined in Agda.TypeChecking.Pretty prettyTCM :: MonadPretty m => WithHiding a -> m Doc Source # | |||||
Normalise t => Normalise (WithHiding t) Source # | |||||
Defined in Agda.TypeChecking.Reduce normalise' :: WithHiding t -> ReduceM (WithHiding t) Source # | |||||
EmbPrj a => EmbPrj (WithHiding a) Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: WithHiding a -> S Int32 Source # icod_ :: WithHiding a -> S Int32 Source # value :: Int32 -> R (WithHiding a) Source # | |||||
Subst a => Subst (WithHiding a) Source # | |||||
Defined in Agda.TypeChecking.Substitute
applySubst :: Substitution' (SubstArg (WithHiding a)) -> WithHiding a -> WithHiding a Source # | |||||
NFData a => NFData (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common rnf :: WithHiding a -> () | |||||
Show a => Show (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> WithHiding a -> ShowS show :: WithHiding a -> String showList :: [WithHiding a] -> ShowS | |||||
Eq a => Eq (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common (==) :: WithHiding a -> WithHiding a -> Bool (/=) :: WithHiding a -> WithHiding a -> Bool | |||||
Ord a => Ord (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common compare :: WithHiding a -> WithHiding a -> Ordering (<) :: WithHiding a -> WithHiding a -> Bool (<=) :: WithHiding a -> WithHiding a -> Bool (>) :: WithHiding a -> WithHiding a -> Bool (>=) :: WithHiding a -> WithHiding a -> Bool max :: WithHiding a -> WithHiding a -> WithHiding a min :: WithHiding a -> WithHiding a -> WithHiding a | |||||
AddContext (List1 (WithHiding Name), Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat Source # | |||||
AddContext ([WithHiding Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source # | |||||
type ConOfAbs (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
type AbsOfCon (WithHiding c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
type SubstArg (WithHiding a) Source # | |||||
Defined in Agda.TypeChecking.Substitute |
Constr a |
Instances
ToConcrete (Constr Constructor) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete
toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor)) Source # bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon b Source # | |||||
type ConOfAbs (Constr Constructor) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete |
data Associativity Source #
Associativity.
Instances
Pretty Associativity Source # | |
Defined in Agda.Syntax.Concrete.Pretty pretty :: Associativity -> Doc Source # prettyPrec :: Int -> Associativity -> Doc Source # prettyList :: [Associativity] -> Doc Source # | |
ToTerm Associativity Source # | |
Defined in Agda.TypeChecking.Primitive | |
EmbPrj Associativity Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: Associativity -> S Int32 Source # icod_ :: Associativity -> S Int32 Source # value :: Int32 -> R Associativity Source # | |
Show Associativity Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> Associativity -> ShowS show :: Associativity -> String showList :: [Associativity] -> ShowS | |
Eq Associativity Source # | |
Defined in Agda.Syntax.Common (==) :: Associativity -> Associativity -> Bool (/=) :: Associativity -> Associativity -> Bool | |
Ord Associativity Source # | |
Defined in Agda.Syntax.Common compare :: Associativity -> Associativity -> Ordering (<) :: Associativity -> Associativity -> Bool (<=) :: Associativity -> Associativity -> Bool (>) :: Associativity -> Associativity -> Bool (>=) :: Associativity -> Associativity -> Bool max :: Associativity -> Associativity -> Associativity min :: Associativity -> Associativity -> Associativity |
data OverlapMode Source #
The possible overlap modes for an instance, also used for instance candidates.
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. |
Instances
HasOverlapMode OverlapMode Source # | |
Defined in Agda.Syntax.Common | |
Pretty OverlapMode Source # | |
Defined in Agda.Syntax.Common pretty :: OverlapMode -> Doc Source # prettyPrec :: Int -> OverlapMode -> Doc Source # prettyList :: [OverlapMode] -> Doc Source # | |
KillRange OverlapMode Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj OverlapMode Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: OverlapMode -> S Int32 Source # icod_ :: OverlapMode -> S Int32 Source # value :: Int32 -> R OverlapMode Source # | |
NFData OverlapMode Source # | |
Defined in Agda.Syntax.Common rnf :: OverlapMode -> () | |
Bounded OverlapMode Source # | |
Defined in Agda.Syntax.Common | |
Enum OverlapMode Source # | |
Defined in Agda.Syntax.Common succ :: OverlapMode -> OverlapMode pred :: OverlapMode -> OverlapMode toEnum :: Int -> OverlapMode fromEnum :: OverlapMode -> Int enumFrom :: OverlapMode -> [OverlapMode] enumFromThen :: OverlapMode -> OverlapMode -> [OverlapMode] enumFromTo :: OverlapMode -> OverlapMode -> [OverlapMode] enumFromThenTo :: OverlapMode -> OverlapMode -> OverlapMode -> [OverlapMode] | |
Show OverlapMode Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> OverlapMode -> ShowS show :: OverlapMode -> String showList :: [OverlapMode] -> ShowS | |
Eq OverlapMode Source # | |
Defined in Agda.Syntax.Common (==) :: OverlapMode -> OverlapMode -> Bool (/=) :: OverlapMode -> OverlapMode -> Bool | |
Ord OverlapMode Source # | |
Defined in Agda.Syntax.Common compare :: OverlapMode -> OverlapMode -> Ordering (<) :: OverlapMode -> OverlapMode -> Bool (<=) :: OverlapMode -> OverlapMode -> Bool (>) :: OverlapMode -> OverlapMode -> Bool (>=) :: OverlapMode -> OverlapMode -> Bool max :: OverlapMode -> OverlapMode -> OverlapMode min :: OverlapMode -> OverlapMode -> OverlapMode |
data Overlappable Source #
Instances
NFData Overlappable Source # | |
Defined in Agda.Syntax.Common rnf :: Overlappable -> () | |
Monoid Overlappable Source # | |
Defined in Agda.Syntax.Common mappend :: Overlappable -> Overlappable -> Overlappable mconcat :: [Overlappable] -> Overlappable | |
Semigroup Overlappable Source # | Just for the |
Defined in Agda.Syntax.Common (<>) :: Overlappable -> Overlappable -> Overlappable # sconcat :: NonEmpty Overlappable -> Overlappable stimes :: Integral b => b -> Overlappable -> Overlappable | |
Show Overlappable Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> Overlappable -> ShowS show :: Overlappable -> String showList :: [Overlappable] -> ShowS | |
Eq Overlappable Source # | |
Defined in Agda.Syntax.Common (==) :: Overlappable -> Overlappable -> Bool (/=) :: Overlappable -> Overlappable -> Bool | |
Ord Overlappable Source # | |
Defined in Agda.Syntax.Common compare :: Overlappable -> Overlappable -> Ordering (<) :: Overlappable -> Overlappable -> Bool (<=) :: Overlappable -> Overlappable -> Bool (>) :: Overlappable -> Overlappable -> Bool (>=) :: Overlappable -> Overlappable -> Bool max :: Overlappable -> Overlappable -> Overlappable min :: Overlappable -> Overlappable -> Overlappable |
isInstance :: LensHiding a => a -> Bool Source #
Instances
Pretty FileType Source # | |||||
EmbPrj FileType Source # | |||||
NFData FileType Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic FileType Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show FileType Source # | |||||
Eq FileType Source # | |||||
Ord FileType Source # | |||||
type Rep FileType Source # | |||||
Defined in Agda.Syntax.Common type Rep FileType = D1 ('MetaData "FileType" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "AgdaFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MdFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RstFileType" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TexFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OrgFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypstFileType" 'PrefixI 'False) (U1 :: Type -> Type)))) |
Does a record come with eta-equality?
Instances
CopatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common copatternMatchingAllowed :: HasEta -> Bool Source # | |
PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common patternMatchingAllowed :: HasEta -> Bool Source # | |
Functor HasEta' Source # | |
Foldable HasEta' Source # | |
Defined in Agda.Syntax.Common fold :: Monoid m => HasEta' m -> m foldMap :: Monoid m => (a -> m) -> HasEta' a -> m foldMap' :: Monoid m => (a -> m) -> HasEta' a -> m foldr :: (a -> b -> b) -> b -> HasEta' a -> b foldr' :: (a -> b -> b) -> b -> HasEta' a -> b foldl :: (b -> a -> b) -> b -> HasEta' a -> b foldl' :: (b -> a -> b) -> b -> HasEta' a -> b foldr1 :: (a -> a -> a) -> HasEta' a -> a foldl1 :: (a -> a -> a) -> HasEta' a -> a elem :: Eq a => a -> HasEta' a -> Bool maximum :: Ord a => HasEta' a -> a minimum :: Ord a => HasEta' a -> a | |
Traversable HasEta' Source # | |
HasRange a => HasRange (HasEta' a) Source # | |
KillRange a => KillRange (HasEta' a) Source # | |
Defined in Agda.Syntax.Common killRange :: KillRangeT (HasEta' a) Source # | |
EmbPrj a => EmbPrj (HasEta' a) Source # | |
NFData a => NFData (HasEta' a) Source # | |
Defined in Agda.Syntax.Common | |
Show a => Show (HasEta' a) Source # | |
Eq a => Eq (HasEta' a) Source # | |
Ord a => Ord (HasEta' a) Source # | |
Defined in Agda.Syntax.Common |
type HasEta = HasEta' PatternOrCopattern Source #
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).
data PatternOrCopattern Source #
For a record without eta, which type of matching do we allow?
PatternMatching | Can match on the record constructor. |
CopatternMatching | Can copattern match using the projections. (Default.) |
Instances
CopatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common copatternMatchingAllowed :: HasEta -> Bool Source # | |
CopatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common copatternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
CopatternMatchingAllowed DataOrRecord Source # | |
Defined in Agda.Syntax.Internal copatternMatchingAllowed :: DataOrRecord -> Bool Source # | |
PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common patternMatchingAllowed :: HasEta -> Bool Source # | |
PatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common patternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
PatternMatchingAllowed DataOrRecord Source # | |
Defined in Agda.Syntax.Internal patternMatchingAllowed :: DataOrRecord -> Bool Source # | |
HasRange PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common getRange :: PatternOrCopattern -> Range Source # | |
KillRange PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common | |
KillRange DataOrRecord Source # | |
Defined in Agda.Syntax.Internal | |
EmbPrj PatternOrCopattern Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: PatternOrCopattern -> S Int32 Source # icod_ :: PatternOrCopattern -> S Int32 Source # value :: Int32 -> R PatternOrCopattern Source # | |
EmbPrj DataOrRecord Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal icode :: DataOrRecord -> S Int32 Source # icod_ :: DataOrRecord -> S Int32 Source # value :: Int32 -> R DataOrRecord Source # | |
NFData PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common rnf :: PatternOrCopattern -> () | |
NFData DataOrRecord | |
Defined in Agda.Syntax.Internal rnf :: DataOrRecord -> () | |
Bounded PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common | |
Enum PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common succ :: PatternOrCopattern -> PatternOrCopattern pred :: PatternOrCopattern -> PatternOrCopattern toEnum :: Int -> PatternOrCopattern fromEnum :: PatternOrCopattern -> Int enumFrom :: PatternOrCopattern -> [PatternOrCopattern] enumFromThen :: PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] enumFromTo :: PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] enumFromThenTo :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] | |
Show PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> PatternOrCopattern -> ShowS show :: PatternOrCopattern -> String showList :: [PatternOrCopattern] -> ShowS | |
Eq PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common (==) :: PatternOrCopattern -> PatternOrCopattern -> Bool (/=) :: PatternOrCopattern -> PatternOrCopattern -> Bool | |
Ord PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common compare :: PatternOrCopattern -> PatternOrCopattern -> Ordering (<) :: PatternOrCopattern -> PatternOrCopattern -> Bool (<=) :: PatternOrCopattern -> PatternOrCopattern -> Bool (>) :: PatternOrCopattern -> PatternOrCopattern -> Bool (>=) :: PatternOrCopattern -> PatternOrCopattern -> Bool max :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern min :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern |
class PatternMatchingAllowed a where Source #
Can we pattern match on the record constructor?
patternMatchingAllowed :: a -> Bool Source #
Instances
PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common patternMatchingAllowed :: HasEta -> Bool Source # | |
PatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common patternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common patternMatchingAllowed :: Induction -> Bool Source # | |
PatternMatchingAllowed DataOrRecord Source # | |
Defined in Agda.Syntax.Internal patternMatchingAllowed :: DataOrRecord -> Bool Source # | |
PatternMatchingAllowed EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base patternMatchingAllowed :: EtaEquality -> Bool Source # |
class CopatternMatchingAllowed a where Source #
Can we construct a record by copattern matching?
copatternMatchingAllowed :: a -> Bool Source #
Instances
CopatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common copatternMatchingAllowed :: HasEta -> Bool Source # | |
CopatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common copatternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
CopatternMatchingAllowed ConHead Source # | |
Defined in Agda.Syntax.Internal copatternMatchingAllowed :: ConHead -> Bool Source # | |
CopatternMatchingAllowed DataOrRecord Source # | |
Defined in Agda.Syntax.Internal copatternMatchingAllowed :: DataOrRecord -> Bool Source # | |
CopatternMatchingAllowed EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base copatternMatchingAllowed :: EtaEquality -> Bool Source # |
class HasOverlapMode a where Source #
Instances
isIncoherent :: HasOverlapMode a => a -> Bool Source #
isOverlappable :: HasOverlapMode a => a -> Bool Source #
isOverlapping :: HasOverlapMode a => a -> Bool Source #
hidingToString :: Hiding -> String Source #
class LensArgInfo a where Source #
getArgInfo :: a -> ArgInfo Source #
setArgInfo :: ArgInfo -> a -> a Source #
mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a Source #
Instances
LensArgInfo ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensArgInfo Definition Source # | |
Defined in Agda.TypeChecking.Monad.Base getArgInfo :: Definition -> ArgInfo Source # setArgInfo :: ArgInfo -> Definition -> Definition Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Definition -> Definition Source # | |
LensArgInfo (Arg a) Source # | |
Defined in Agda.Syntax.Common | |
LensArgInfo (FlexibleVar a) Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem getArgInfo :: FlexibleVar a -> ArgInfo Source # setArgInfo :: ArgInfo -> FlexibleVar a -> FlexibleVar a Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a Source # | |
LensArgInfo (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal |
mergeHiding :: LensHiding a => WithHiding a -> a Source #
Monoidal composition of Hiding
information in some data.
notVisible :: LensHiding a => a -> Bool Source #
LensHiding a => a -> Bool Source #
::Hidden
arguments are hidden
.
hide :: LensHiding a => a -> a Source #
hideOrKeepInstance :: LensHiding a => a -> a Source #
makeInstance :: LensHiding a => a -> a Source #
makeInstance' :: LensHiding a => Overlappable -> a -> a Source #
isYesOverlap :: LensHiding a => a -> Bool Source #
sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool Source #
Ignores Overlappable
.
newtype UnderAddition t Source #
Type wrapper to indicate additive monoid/semigroup context.
Instances
Applicative UnderAddition Source # | |
Defined in Agda.Syntax.Common pure :: a -> UnderAddition a (<*>) :: UnderAddition (a -> b) -> UnderAddition a -> UnderAddition b # liftA2 :: (a -> b -> c) -> UnderAddition a -> UnderAddition b -> UnderAddition c (*>) :: UnderAddition a -> UnderAddition b -> UnderAddition b (<*) :: UnderAddition a -> UnderAddition b -> UnderAddition a | |
Functor UnderAddition Source # | |
Defined in Agda.Syntax.Common fmap :: (a -> b) -> UnderAddition a -> UnderAddition b (<$) :: a -> UnderAddition b -> UnderAddition a # | |
POMonoid (UnderAddition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderAddition Modality) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderAddition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderAddition Modality) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
PartialOrd t => PartialOrd (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common comparable :: Comparable (UnderAddition t) Source # | |
Monoid (UnderAddition Cohesion) Source # |
|
Defined in Agda.Syntax.Common | |
Monoid (UnderAddition Modality) Source # | Pointwise additive unit. |
Defined in Agda.Syntax.Common | |
Monoid (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
Monoid (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
Semigroup (UnderAddition Cohesion) Source # |
|
Defined in Agda.Syntax.Common (<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion # sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion | |
Semigroup (UnderAddition Modality) Source # | Pointwise addition. |
Defined in Agda.Syntax.Common (<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality # sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality | |
Semigroup (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common (<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity # sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity | |
Semigroup (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common (<>) :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance # sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance | |
Show t => Show (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> UnderAddition t -> ShowS show :: UnderAddition t -> String showList :: [UnderAddition t] -> ShowS | |
Eq t => Eq (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common (==) :: UnderAddition t -> UnderAddition t -> Bool (/=) :: UnderAddition t -> UnderAddition t -> Bool | |
Ord t => Ord (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common compare :: UnderAddition t -> UnderAddition t -> Ordering (<) :: UnderAddition t -> UnderAddition t -> Bool (<=) :: UnderAddition t -> UnderAddition t -> Bool (>) :: UnderAddition t -> UnderAddition t -> Bool (>=) :: UnderAddition t -> UnderAddition t -> Bool max :: UnderAddition t -> UnderAddition t -> UnderAddition t min :: UnderAddition t -> UnderAddition t -> UnderAddition t |
newtype UnderComposition t Source #
Type wrapper to indicate composition or multiplicative monoid/semigroup context.
Instances
Applicative UnderComposition Source # | |
Defined in Agda.Syntax.Common pure :: a -> UnderComposition a (<*>) :: UnderComposition (a -> b) -> UnderComposition a -> UnderComposition b # liftA2 :: (a -> b -> c) -> UnderComposition a -> UnderComposition b -> UnderComposition c (*>) :: UnderComposition a -> UnderComposition b -> UnderComposition b (<*) :: UnderComposition a -> UnderComposition b -> UnderComposition a | |
Functor UnderComposition Source # | |
Defined in Agda.Syntax.Common fmap :: (a -> b) -> UnderComposition a -> UnderComposition b (<$) :: a -> UnderComposition b -> UnderComposition a # | |
LeftClosedPOMonoid (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
LeftClosedPOMonoid (UnderComposition Modality) Source # | |
Defined in Agda.Syntax.Common | |
LeftClosedPOMonoid (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
LeftClosedPOMonoid (UnderComposition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderComposition Modality) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderComposition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderComposition Modality) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderComposition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
PartialOrd t => PartialOrd (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common comparable :: Comparable (UnderComposition t) Source # | |
Monoid (UnderComposition Cohesion) Source # |
|
Monoid (UnderComposition Modality) Source # | Pointwise composition unit. |
Monoid (UnderComposition Quantity) Source # | In the absense of finite quantities besides 0, ω is the unit. Otherwise, 1 is the unit. |
Monoid (UnderComposition Relevance) Source # |
|
Semigroup (UnderComposition Cohesion) Source # |
|
Defined in Agda.Syntax.Common (<>) :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion # sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion | |
Semigroup (UnderComposition Erased) Source # | |
Defined in Agda.Syntax.Common (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased | |
Semigroup (UnderComposition Modality) Source # | Pointwise composition. |
Defined in Agda.Syntax.Common (<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality # sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality | |
Semigroup (UnderComposition Quantity) Source # | Composition of quantities (multiplication).
Right-biased for origin. |
Defined in Agda.Syntax.Common (<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity | |
Semigroup (UnderComposition Relevance) Source # |
|
Defined in Agda.Syntax.Common (<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance # sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance | |
Show t => Show (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> UnderComposition t -> ShowS show :: UnderComposition t -> String showList :: [UnderComposition t] -> ShowS | |
Eq t => Eq (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common (==) :: UnderComposition t -> UnderComposition t -> Bool (/=) :: UnderComposition t -> UnderComposition t -> Bool | |
Ord t => Ord (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common compare :: UnderComposition t -> UnderComposition t -> Ordering (<) :: UnderComposition t -> UnderComposition t -> Bool (<=) :: UnderComposition t -> UnderComposition t -> Bool (>) :: UnderComposition t -> UnderComposition t -> Bool (>=) :: UnderComposition t -> UnderComposition t -> Bool max :: UnderComposition t -> UnderComposition t -> UnderComposition t min :: UnderComposition t -> UnderComposition t -> UnderComposition t |
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.
Quantity0 Q0Origin | Zero uses |
Quantity1 Q1Origin | Linear use |
Quantityω QωOrigin | Unrestricted use |
Instances
LensQuantity Quantity Source # | |||||
Defined in Agda.Syntax.Common | |||||
Pretty Quantity Source # | |||||
HasRange Quantity Source # | |||||
KillRange Quantity Source # | |||||
Defined in Agda.Syntax.Common | |||||
SetRange Quantity Source # | |||||
Verbalize Quantity Source # | |||||
Defined in Agda.TypeChecking.Errors | |||||
PrettyTCM Quantity Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
EmbPrj Quantity Source # | |||||
Unquote Quantity Source # | |||||
PartialOrd Quantity Source # | Note that the order is | ||||
Defined in Agda.Syntax.Common | |||||
NFData Quantity Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic Quantity Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show Quantity Source # | |||||
Eq Quantity Source # | |||||
Ord Quantity Source # | |||||
LeftClosedPOMonoid (UnderComposition Quantity) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POMonoid (UnderAddition Quantity) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POMonoid (UnderComposition Quantity) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POSemigroup (UnderAddition Quantity) Source # | |||||
Defined in Agda.Syntax.Common | |||||
POSemigroup (UnderComposition Quantity) Source # | |||||
Defined in Agda.Syntax.Common | |||||
Monoid (UnderAddition Quantity) Source # | |||||
Defined in Agda.Syntax.Common | |||||
Monoid (UnderComposition Quantity) Source # | In the absense of finite quantities besides 0, ω is the unit. Otherwise, 1 is the unit. | ||||
Semigroup (UnderAddition Quantity) Source # | |||||
Defined in Agda.Syntax.Common (<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity # sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity | |||||
Semigroup (UnderComposition Quantity) Source # | Composition of quantities (multiplication).
Right-biased for origin. | ||||
Defined in Agda.Syntax.Common (<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity | |||||
type Rep Quantity Source # | |||||
Defined in Agda.Syntax.Common type Rep Quantity = D1 ('MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Quantity0" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q0Origin)) :+: (C1 ('MetaCons "Quantity1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q1Origin)) :+: C1 ('MetaCons "Quantity\969" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QωOrigin)))) |
composeModality :: Modality -> Modality -> Modality Source #
Multiplicative monoid (standard monoid).
unitModality :: Modality Source #
Identity under composition
inverseComposeModality :: Modality -> Modality -> Modality Source #
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).
zeroModality :: Modality Source #
Identity under addition
moreUsableModality :: Modality -> Modality -> Bool Source #
m
means that an moreUsableModality
m'm
can be used
where ever an m'
is required.
usableModality :: LensModality a => a -> Bool Source #
class LensModality a where Source #
Nothing
getModality :: a -> Modality Source #
default getModality :: LensArgInfo a => a -> Modality Source #
setModality :: Modality -> a -> a Source #
mapModality :: (Modality -> Modality) -> a -> a Source #
default mapModality :: LensArgInfo a => (Modality -> Modality) -> a -> a Source #
Instances
LensModality ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensModality Modality Source # | |
Defined in Agda.Syntax.Common | |
LensModality Definition Source # | |
Defined in Agda.TypeChecking.Monad.Base getModality :: Definition -> Modality Source # setModality :: Modality -> Definition -> Definition Source # mapModality :: (Modality -> Modality) -> Definition -> Definition Source # | |
LensModality MetaInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
LensModality MetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base getModality :: MetaVariable -> Modality Source # setModality :: Modality -> MetaVariable -> MetaVariable Source # mapModality :: (Modality -> Modality) -> MetaVariable -> MetaVariable Source # | |
LensModality RemoteMetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base getModality :: RemoteMetaVariable -> Modality Source # setModality :: Modality -> RemoteMetaVariable -> RemoteMetaVariable Source # mapModality :: (Modality -> Modality) -> RemoteMetaVariable -> RemoteMetaVariable Source # | |
LensModality (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
LensModality (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
LensModality (FlexibleVar a) Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem getModality :: FlexibleVar a -> Modality Source # setModality :: Modality -> FlexibleVar a -> FlexibleVar a Source # mapModality :: (Modality -> Modality) -> FlexibleVar a -> FlexibleVar a Source # | |
LensModality (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal | |
LensModality (FreeEnv' a b c) Source # | |
Defined in Agda.TypeChecking.Free.Lazy |
usableRelevance :: LensRelevance a => a -> Bool Source #
usableRelevance rel == False
iff we cannot use a variable of rel
.
usableQuantity :: LensQuantity a => a -> Bool Source #
A thing of quantity 0 is unusable, all others are usable.
usableCohesion :: LensCohesion a => a -> Bool Source #
usableCohesion rel == False
iff we cannot use a variable of rel
.
composeRelevance :: Relevance -> Relevance -> Relevance Source #
Relevance
composition.
Irrelevant
is dominant, Relevant
is neutral.
Composition coincides with max
.
composeCohesion :: Cohesion -> Cohesion -> Cohesion Source #
Cohesion
composition.
Squash
is dominant, Continuous
is neutral.
applyModality :: LensModality a => Modality -> a -> a Source #
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
.
inverseComposeRelevance :: Relevance -> Relevance -> Relevance Source #
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).
inverseComposeQuantity :: Quantity -> Quantity -> Quantity Source #
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).
inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion Source #
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
.
inverseApplyModalityButNotQuantity :: LensModality a => Modality -> a -> a Source #
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.
class LensQuantity a where Source #
Nothing
getQuantity :: a -> Quantity Source #
default getQuantity :: LensModality a => a -> Quantity Source #
setQuantity :: Quantity -> a -> a Source #
mapQuantity :: (Quantity -> Quantity) -> a -> a Source #
default mapQuantity :: LensModality a => (Quantity -> Quantity) -> a -> a Source #
Instances
LensQuantity ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity Modality Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity Quantity Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity Definition Source # | |
Defined in Agda.TypeChecking.Monad.Base getQuantity :: Definition -> Quantity Source # setQuantity :: Quantity -> Definition -> Definition Source # mapQuantity :: (Quantity -> Quantity) -> Definition -> Definition Source # | |
LensQuantity MetaInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
LensQuantity MetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base getQuantity :: MetaVariable -> Quantity Source # setQuantity :: Quantity -> MetaVariable -> MetaVariable Source # mapQuantity :: (Quantity -> Quantity) -> MetaVariable -> MetaVariable Source # | |
LensQuantity RemoteMetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base getQuantity :: RemoteMetaVariable -> Quantity Source # setQuantity :: Quantity -> RemoteMetaVariable -> RemoteMetaVariable Source # mapQuantity :: (Quantity -> Quantity) -> RemoteMetaVariable -> RemoteMetaVariable Source # | |
LensQuantity (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
LensQuantity (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal | |
LensQuantity (FreeEnv' a b c) Source # | |
Defined in Agda.TypeChecking.Free.Lazy |
Origin of Quantity1
.
Q1Inferred | User wrote nothing. |
Q1 Range | User wrote "@1". |
Q1Linear Range | User wrote "@linear". |
Instances
Pretty Q1Origin Source # | |||||
HasRange Q1Origin Source # | |||||
KillRange Q1Origin Source # | |||||
Defined in Agda.Syntax.Common | |||||
SetRange Q1Origin Source # | |||||
EmbPrj Q1Origin Source # | |||||
Null Q1Origin Source # | |||||
NFData Q1Origin Source # | |||||
Defined in Agda.Syntax.Common | |||||
Monoid Q1Origin Source # | |||||
Semigroup Q1Origin Source # | Right-biased composition, because the left quantity acts as context, and the right one as occurrence. | ||||
Generic Q1Origin Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show Q1Origin Source # | |||||
Eq Q1Origin Source # | |||||
Ord Q1Origin Source # | |||||
type Rep Q1Origin Source # | |||||
Defined in Agda.Syntax.Common type Rep Q1Origin = D1 ('MetaData "Q1Origin" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Q1Inferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Q1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q1Linear" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) |
addRelevance :: Relevance -> Relevance -> Relevance Source #
Combine inferred Relevance
.
The unit is Irrelevant
.
addQuantity :: Quantity -> Quantity -> Quantity Source #
Quantity
forms an additive monoid with zero Quantity0.
zeroRelevance :: Relevance Source #
Relevance
forms a monoid under addition, and even a semiring.
zeroQuantity :: Quantity Source #
Identity element under addition
zeroCohesion :: Cohesion Source #
Cohesion
forms a monoid under addition, and even a semiring.
unitRelevance :: Relevance Source #
Identity element under composition
unitQuantity :: Quantity Source #
Identity element under composition
unitCohesion :: Cohesion Source #
Identity under composition
topModality :: Modality Source #
Absorptive element under addition.
topRelevance :: Relevance Source #
Absorptive element under addition.
topQuantity :: Quantity Source #
Absorptive element is ω.
topCohesion :: Cohesion Source #
Absorptive element under addition.
defaultModality :: Modality Source #
The default Modality Beware that this is neither the additive unit nor the unit under composition, because the default quantity is ω.
defaultRelevance :: Relevance Source #
Default Relevance is the identity element under composition
defaultQuantity :: Quantity Source #
Absorptive element! This differs from Relevance and Cohesion whose default is the multiplicative unit.
defaultCohesion :: Cohesion Source #
Default Cohesion is the identity element under composition
sameModality :: (LensModality a, LensModality b) => a -> b -> Bool Source #
Equality ignoring origin.
sameRelevance :: Relevance -> Relevance -> Bool Source #
Equality ignoring origin.
sameQuantity :: Quantity -> Quantity -> Bool Source #
Equality ignoring origin.
sameCohesion :: Cohesion -> Cohesion -> Bool Source #
Equality ignoring origin.
class LensCohesion a where Source #
A lens to access the Cohesion
attribute in data structures.
Minimal implementation: getCohesion
and mapCohesion
or LensModality
.
Nothing
getCohesion :: a -> Cohesion Source #
default getCohesion :: LensModality a => a -> Cohesion Source #
setCohesion :: Cohesion -> a -> a Source #
mapCohesion :: (Cohesion -> Cohesion) -> a -> a Source #
default mapCohesion :: LensModality a => (Cohesion -> Cohesion) -> a -> a Source #
Instances
LensCohesion ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensCohesion Cohesion Source # | |
Defined in Agda.Syntax.Common | |
LensCohesion Modality Source # | |
Defined in Agda.Syntax.Common | |
LensCohesion (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
LensCohesion (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal |
getRelevanceMod :: LensModality a => LensGet a Relevance Source #
setRelevanceMod :: LensModality a => LensSet a Relevance Source #
mapRelevanceMod :: LensModality a => LensMap a Relevance Source #
getQuantityMod :: LensModality a => LensGet a Quantity Source #
setQuantityMod :: LensModality a => LensSet a Quantity Source #
mapQuantityMod :: LensModality a => LensMap a Quantity Source #
getCohesionMod :: LensModality a => LensGet a Cohesion Source #
setCohesionMod :: LensModality a => LensSet a Cohesion Source #
mapCohesionMod :: LensModality a => LensMap a Cohesion Source #
Origin of Quantity0
.
Q0Inferred | User wrote nothing. |
Q0 Range | User wrote "@0". |
Q0Erased Range | User wrote "@erased". |
Instances
Pretty Q0Origin Source # | |||||
HasRange Q0Origin Source # | |||||
KillRange Q0Origin Source # | |||||
Defined in Agda.Syntax.Common | |||||
SetRange Q0Origin Source # | |||||
EmbPrj Q0Origin Source # | |||||
Null Q0Origin Source # | |||||
NFData Q0Origin Source # | |||||
Defined in Agda.Syntax.Common | |||||
Monoid Q0Origin Source # | |||||
Semigroup Q0Origin Source # | Right-biased composition, because the left quantity acts as context, and the right one as occurrence. | ||||
Generic Q0Origin Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show Q0Origin Source # | |||||
Eq Q0Origin Source # | |||||
Ord Q0Origin Source # | |||||
type Rep Q0Origin Source # | |||||
Defined in Agda.Syntax.Common type Rep Q0Origin = D1 ('MetaData "Q0Origin" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Q0Inferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Q0" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q0Erased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) |
Origin of Quantityω
.
QωInferred | User wrote nothing. |
Qω Range | User wrote "@ω". |
QωPlenty Range | User wrote "@plenty". |
Instances
Pretty QωOrigin Source # | |||||
HasRange QωOrigin Source # | |||||
KillRange QωOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
SetRange QωOrigin Source # | |||||
EmbPrj QωOrigin Source # | |||||
Null QωOrigin Source # | |||||
NFData QωOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
Monoid QωOrigin Source # | |||||
Semigroup QωOrigin Source # | Right-biased composition, because the left quantity acts as context, and the right one as occurrence. | ||||
Generic QωOrigin Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show QωOrigin Source # | |||||
Eq QωOrigin Source # | |||||
Ord QωOrigin Source # | |||||
type Rep QωOrigin Source # | |||||
Defined in Agda.Syntax.Common type Rep QωOrigin = D1 ('MetaData "Q\969Origin" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Q\969Inferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Q\969" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Q\969Plenty" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) |
moreQuantity :: Quantity -> Quantity -> Bool Source #
m
means that an moreUsableQuantity
m'm
can be used
where ever an m'
is required.
applyQuantity :: LensQuantity a => Quantity -> a -> a Source #
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
.
inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a Source #
Left division by a Quantity
.
Used e.g. to modify context when going into a q
argument.
hasQuantity1 :: LensQuantity a => a -> Bool Source #
Check for Quantity1
.
hasQuantityω :: LensQuantity a => a -> Bool Source #
Check for Quantityω
.
noUserQuantity :: LensQuantity a => a -> Bool Source #
Did the user supply a quantity annotation?
isQuantityω :: LensQuantity a => a -> Bool Source #
A special case of Quantity
: erased or not.
Note that the Ord
instance does *not* ignore the origin
arguments.
Instances
Pretty Erased Source # | |||||
HasRange Erased Source # | |||||
KillRange Erased Source # | |||||
Defined in Agda.Syntax.Common | |||||
PrettyTCM Erased Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
NFData Erased Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic Erased Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show Erased Source # | |||||
Eq Erased Source # | |||||
Ord Erased Source # | |||||
Semigroup (UnderComposition Erased) Source # | |||||
Defined in Agda.Syntax.Common (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased | |||||
type Rep Erased Source # | |||||
Defined in Agda.Syntax.Common type Rep Erased = D1 ('MetaData "Erased" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Erased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q0Origin)) :+: C1 ('MetaCons "NotErased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QωOrigin))) |
defaultErased :: Erased Source #
The default value of type Erased
: not erased.
sameErased :: Erased -> Erased -> Bool Source #
Equality ignoring origin.
allRelevances :: [Relevance] Source #
isRelevant :: LensRelevance a => a -> Bool Source #
isIrrelevant :: LensRelevance a => a -> Bool Source #
isNonStrict :: LensRelevance a => a -> Bool Source #
moreRelevant :: Relevance -> Relevance -> Bool Source #
Information ordering.
Relevant `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
applyRelevance :: LensRelevance a => Relevance -> a -> a Source #
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
.
inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a Source #
Left division by a Relevance
.
Used e.g. to modify context when going into a rel
argument.
irrToNonStrict :: Relevance -> Relevance Source #
Irrelevant function arguments may appear non-strictly in the codomain type.
nonStrictToRel :: Relevance -> Relevance Source #
Applied when working on types (unless --experimental-irrelevance).
nonStrictToIrr :: Relevance -> Relevance Source #
data Annotation Source #
We have a tuple of annotations, which might not be fully orthogonal.
Instances
LensAnnotation Annotation Source # | |||||
Defined in Agda.Syntax.Common getAnnotation :: Annotation -> Annotation Source # setAnnotation :: Annotation -> Annotation -> Annotation Source # mapAnnotation :: (Annotation -> Annotation) -> Annotation -> Annotation Source # | |||||
HasRange Annotation Source # | |||||
Defined in Agda.Syntax.Common getRange :: Annotation -> Range Source # | |||||
KillRange Annotation Source # | |||||
Defined in Agda.Syntax.Common | |||||
EmbPrj Annotation Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: Annotation -> S Int32 Source # icod_ :: Annotation -> S Int32 Source # value :: Int32 -> R Annotation Source # | |||||
NFData Annotation Source # | |||||
Defined in Agda.Syntax.Common rnf :: Annotation -> () | |||||
Generic Annotation Source # | |||||
Defined in Agda.Syntax.Common
from :: Annotation -> Rep Annotation x to :: Rep Annotation x -> Annotation | |||||
Show Annotation Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> Annotation -> ShowS show :: Annotation -> String showList :: [Annotation] -> ShowS | |||||
Eq Annotation Source # | |||||
Defined in Agda.Syntax.Common (==) :: Annotation -> Annotation -> Bool (/=) :: Annotation -> Annotation -> Bool | |||||
Ord Annotation Source # | |||||
Defined in Agda.Syntax.Common compare :: Annotation -> Annotation -> Ordering (<) :: Annotation -> Annotation -> Bool (<=) :: Annotation -> Annotation -> Bool (>) :: Annotation -> Annotation -> Bool (>=) :: Annotation -> Annotation -> Bool max :: Annotation -> Annotation -> Annotation min :: Annotation -> Annotation -> Annotation | |||||
type Rep Annotation Source # | |||||
Defined in Agda.Syntax.Common type Rep Annotation = D1 ('MetaData "Annotation" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Annotation" 'PrefixI 'True) (S1 ('MetaSel ('Just "annLock") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lock))) |
defaultLock :: Lock Source #
class LensAnnotation a where Source #
Nothing
getAnnotation :: a -> Annotation Source #
default getAnnotation :: LensArgInfo a => a -> Annotation Source #
setAnnotation :: Annotation -> a -> a Source #
default setAnnotation :: LensArgInfo a => Annotation -> a -> a Source #
mapAnnotation :: (Annotation -> Annotation) -> a -> a Source #
Instances
LensAnnotation Annotation Source # | |
Defined in Agda.Syntax.Common getAnnotation :: Annotation -> Annotation Source # setAnnotation :: Annotation -> Annotation -> Annotation Source # mapAnnotation :: (Annotation -> Annotation) -> Annotation -> Annotation Source # | |
LensAnnotation ArgInfo Source # | |
Defined in Agda.Syntax.Common getAnnotation :: ArgInfo -> Annotation Source # setAnnotation :: Annotation -> ArgInfo -> ArgInfo Source # mapAnnotation :: (Annotation -> Annotation) -> ArgInfo -> ArgInfo Source # | |
LensAnnotation (Arg t) Source # | |
Defined in Agda.Syntax.Common getAnnotation :: Arg t -> Annotation Source # setAnnotation :: Annotation -> Arg t -> Arg t Source # mapAnnotation :: (Annotation -> Annotation) -> Arg t -> Arg t Source # | |
LensAnnotation (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal getAnnotation :: Dom' t e -> Annotation Source # setAnnotation :: Annotation -> Dom' t e -> Dom' t e Source # mapAnnotation :: (Annotation -> Annotation) -> Dom' t e -> Dom' t e Source # |
data LockOrigin Source #
Instances
Bounded LockOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum LockOrigin Source # | |||||
Defined in Agda.Syntax.Common succ :: LockOrigin -> LockOrigin pred :: LockOrigin -> LockOrigin toEnum :: Int -> LockOrigin fromEnum :: LockOrigin -> Int enumFrom :: LockOrigin -> [LockOrigin] enumFromThen :: LockOrigin -> LockOrigin -> [LockOrigin] enumFromTo :: LockOrigin -> LockOrigin -> [LockOrigin] enumFromThenTo :: LockOrigin -> LockOrigin -> LockOrigin -> [LockOrigin] | |||||
Generic LockOrigin Source # | |||||
Defined in Agda.Syntax.Common
from :: LockOrigin -> Rep LockOrigin x to :: Rep LockOrigin x -> LockOrigin | |||||
Show LockOrigin Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> LockOrigin -> ShowS show :: LockOrigin -> String showList :: [LockOrigin] -> ShowS | |||||
Eq LockOrigin Source # | |||||
Defined in Agda.Syntax.Common (==) :: LockOrigin -> LockOrigin -> Bool (/=) :: LockOrigin -> LockOrigin -> Bool | |||||
Ord LockOrigin Source # | |||||
Defined in Agda.Syntax.Common compare :: LockOrigin -> LockOrigin -> Ordering (<) :: LockOrigin -> LockOrigin -> Bool (<=) :: LockOrigin -> LockOrigin -> Bool (>) :: LockOrigin -> LockOrigin -> Bool (>=) :: LockOrigin -> LockOrigin -> Bool max :: LockOrigin -> LockOrigin -> LockOrigin min :: LockOrigin -> LockOrigin -> LockOrigin | |||||
type Rep LockOrigin Source # | |||||
Defined in Agda.Syntax.Common type Rep LockOrigin = D1 ('MetaData "LockOrigin" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "LockOLock" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LockOTick" 'PrefixI 'False) (U1 :: Type -> Type)) |
allCohesions :: [Cohesion] Source #
isContinuous :: LensCohesion a => a -> Bool Source #
moreCohesion :: Cohesion -> Cohesion -> Bool Source #
Information ordering.
Flat `moreCohesion`
Continuous `moreCohesion`
Sharp `moreCohesion`
Squash
applyCohesion :: LensCohesion a => Cohesion -> a -> a Source #
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
.
inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a Source #
Left division by a Cohesion
.
Used e.g. to modify context when going into a rel
argument.
data FreeVariables Source #
UnknownFVs | |
KnownFVs IntSet |
Instances
LensFreeVariables FreeVariables Source # | |
Defined in Agda.Syntax.Common | |
KillRange FreeVariables Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj FreeVariables Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: FreeVariables -> S Int32 Source # icod_ :: FreeVariables -> S Int32 Source # value :: Int32 -> R FreeVariables Source # | |
NFData FreeVariables Source # | |
Defined in Agda.Syntax.Common rnf :: FreeVariables -> () | |
Monoid FreeVariables Source # | |
Defined in Agda.Syntax.Common mappend :: FreeVariables -> FreeVariables -> FreeVariables mconcat :: [FreeVariables] -> FreeVariables | |
Semigroup FreeVariables Source # | |
Defined in Agda.Syntax.Common (<>) :: FreeVariables -> FreeVariables -> FreeVariables # sconcat :: NonEmpty FreeVariables -> FreeVariables stimes :: Integral b => b -> FreeVariables -> FreeVariables | |
Show FreeVariables Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> FreeVariables -> ShowS show :: FreeVariables -> String showList :: [FreeVariables] -> ShowS | |
Eq FreeVariables Source # | |
Defined in Agda.Syntax.Common (==) :: FreeVariables -> FreeVariables -> Bool (/=) :: FreeVariables -> FreeVariables -> Bool | |
Ord FreeVariables Source # | |
Defined in Agda.Syntax.Common compare :: FreeVariables -> FreeVariables -> Ordering (<) :: FreeVariables -> FreeVariables -> Bool (<=) :: FreeVariables -> FreeVariables -> Bool (>) :: FreeVariables -> FreeVariables -> Bool (>=) :: FreeVariables -> FreeVariables -> Bool max :: FreeVariables -> FreeVariables -> FreeVariables min :: FreeVariables -> FreeVariables -> FreeVariables |
oneFreeVariable :: Int -> FreeVariables Source #
freeVariablesFromList :: [Int] -> FreeVariables Source #
class LensFreeVariables a where Source #
A lens to access the FreeVariables
attribute in data structures.
Minimal implementation: getFreeVariables
and mapFreeVariables
or LensArgInfo
.
Nothing
getFreeVariables :: a -> FreeVariables Source #
default getFreeVariables :: LensArgInfo a => a -> FreeVariables Source #
setFreeVariables :: FreeVariables -> a -> a Source #
mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a Source #
default mapFreeVariables :: LensArgInfo a => (FreeVariables -> FreeVariables) -> a -> a Source #
Instances
LensFreeVariables ArgInfo Source # | |
Defined in Agda.Syntax.Common getFreeVariables :: ArgInfo -> FreeVariables Source # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo Source # | |
LensFreeVariables FreeVariables Source # | |
Defined in Agda.Syntax.Common | |
LensFreeVariables (Arg e) Source # | |
Defined in Agda.Syntax.Common getFreeVariables :: Arg e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Arg e -> Arg e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e Source # | |
LensFreeVariables (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal getFreeVariables :: Dom' t e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Dom' t e -> Dom' t e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom' t e -> Dom' t e Source # |
hasNoFreeVariables :: LensFreeVariables a => a -> Bool Source #
getHidingArgInfo :: LensArgInfo a => LensGet a Hiding Source #
setHidingArgInfo :: LensArgInfo a => LensSet a Hiding Source #
mapHidingArgInfo :: LensArgInfo a => LensMap a Hiding Source #
getModalityArgInfo :: LensArgInfo a => LensGet a Modality Source #
setModalityArgInfo :: LensArgInfo a => LensSet a Modality Source #
mapModalityArgInfo :: LensArgInfo a => LensMap a Modality Source #
getOriginArgInfo :: LensArgInfo a => LensGet a Origin Source #
setOriginArgInfo :: LensArgInfo a => LensSet a Origin Source #
mapOriginArgInfo :: LensArgInfo a => LensMap a Origin Source #
isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool Source #
withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] Source #
class Eq a => Underscore a where Source #
underscore :: a Source #
isUnderscore :: a -> Bool Source #
Instances
Underscore Expr Source # | |
Defined in Agda.Syntax.Abstract underscore :: Expr Source # isUnderscore :: Expr -> Bool Source # | |
Underscore Doc Source # | |
Defined in Agda.Syntax.Common underscore :: Doc Source # isUnderscore :: Doc -> Bool Source # | |
Underscore Name Source # | |
Defined in Agda.Syntax.Concrete.Name underscore :: Name Source # isUnderscore :: Name -> Bool Source # | |
Underscore QName Source # | |
Defined in Agda.Syntax.Concrete.Name underscore :: QName Source # isUnderscore :: QName -> Bool Source # | |
Underscore ByteString Source # | |
Defined in Agda.Syntax.Common underscore :: ByteString Source # isUnderscore :: ByteString -> Bool Source # | |
Underscore String Source # | |
Defined in Agda.Syntax.Common underscore :: String Source # isUnderscore :: String -> Bool Source # |
class LensNamed a where Source #
Accessor/editor for the nameOf
component.
Nothing
The type of the name
Instances
type NameOf (Arg a) Source # | |
Defined in Agda.Syntax.Common | |
type NameOf (Maybe a) Source # | |
Defined in Agda.Syntax.Common | |
type NameOf (Named name a) Source # | |
Defined in Agda.Syntax.Common | |
type NameOf (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal |
namedSame :: (LensNamed a, LensNamed b, NameOf a ~ NamedName, NameOf b ~ NamedName) => a -> b -> Bool Source #
fittingNamedArg :: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) => arg -> dom -> Maybe Bool Source #
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
@
defaultNamedArg :: a -> NamedArg a Source #
unnamedArg :: ArgInfo -> a -> NamedArg a Source #
updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b Source #
The functor instance for NamedArg
would be ambiguous,
so we give it another name here.
updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b) Source #
setNamedArg :: NamedArg a -> b -> NamedArg b Source #
setNamedArg a b = updateNamedArg (const b) a
argNameToString :: ArgName -> String Source #
stringToArgName :: String -> ArgName Source #
rawNameToString :: RawName -> String Source #
stringToRawName :: String -> RawName Source #
bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin Source #
Prefer user-written over system-inserted.
Functions can be defined in both infix and prefix style. See
LHS
.
Access modifier.
PrivateAccess KwRange Origin | Store the |
PublicAccess |
data IsAbstract Source #
Abstract or concrete.
Instances
AnyIsAbstract IsAbstract Source # | |||||
Defined in Agda.Syntax.Common anyIsAbstract :: IsAbstract -> IsAbstract Source # | |||||
LensIsAbstract IsAbstract Source # | |||||
Defined in Agda.Syntax.Common | |||||
KillRange IsAbstract Source # | |||||
Defined in Agda.Syntax.Common | |||||
EmbPrj IsAbstract Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: IsAbstract -> S Int32 Source # icod_ :: IsAbstract -> S Int32 Source # value :: Int32 -> R IsAbstract Source # | |||||
Boolean IsAbstract Source # | |||||
Defined in Agda.Syntax.Common fromBool :: Bool -> IsAbstract Source # true :: IsAbstract Source # false :: IsAbstract Source # not :: IsAbstract -> IsAbstract Source # (&&) :: IsAbstract -> IsAbstract -> IsAbstract Source # (||) :: IsAbstract -> IsAbstract -> IsAbstract Source # implies :: IsAbstract -> IsAbstract -> IsAbstract Source # butNot :: IsAbstract -> IsAbstract -> IsAbstract Source # | |||||
IsBool IsAbstract Source # | |||||
Defined in Agda.Syntax.Common toBool :: IsAbstract -> Bool Source # ifThenElse :: IsAbstract -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> IsAbstract -> IsAbstract Source # fromBool2 :: (Bool -> Bool -> Bool) -> IsAbstract -> IsAbstract -> IsAbstract Source # | |||||
NFData IsAbstract Source # | |||||
Defined in Agda.Syntax.Common rnf :: IsAbstract -> () | |||||
Monoid IsAbstract Source # | Default is | ||||
Defined in Agda.Syntax.Common mempty :: IsAbstract mappend :: IsAbstract -> IsAbstract -> IsAbstract mconcat :: [IsAbstract] -> IsAbstract | |||||
Semigroup IsAbstract Source # | Semigroup computes if any of several is an | ||||
Defined in Agda.Syntax.Common (<>) :: IsAbstract -> IsAbstract -> IsAbstract # sconcat :: NonEmpty IsAbstract -> IsAbstract stimes :: Integral b => b -> IsAbstract -> IsAbstract | |||||
Generic IsAbstract Source # | |||||
Defined in Agda.Syntax.Common
from :: IsAbstract -> Rep IsAbstract x to :: Rep IsAbstract x -> IsAbstract | |||||
Show IsAbstract Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> IsAbstract -> ShowS show :: IsAbstract -> String showList :: [IsAbstract] -> ShowS | |||||
Eq IsAbstract Source # | |||||
Defined in Agda.Syntax.Common (==) :: IsAbstract -> IsAbstract -> Bool (/=) :: IsAbstract -> IsAbstract -> Bool | |||||
Ord IsAbstract Source # | |||||
Defined in Agda.Syntax.Common compare :: IsAbstract -> IsAbstract -> Ordering (<) :: IsAbstract -> IsAbstract -> Bool (<=) :: IsAbstract -> IsAbstract -> Bool (>) :: IsAbstract -> IsAbstract -> Bool (>=) :: IsAbstract -> IsAbstract -> Bool max :: IsAbstract -> IsAbstract -> IsAbstract min :: IsAbstract -> IsAbstract -> IsAbstract | |||||
type Rep IsAbstract Source # | |||||
Defined in Agda.Syntax.Common type Rep IsAbstract = D1 ('MetaData "IsAbstract" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "AbstractDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConcreteDef" 'PrefixI 'False) (U1 :: Type -> Type)) |
class LensIsAbstract a where Source #
lensIsAbstract :: Lens' a IsAbstract Source #
Instances
LensIsAbstract IsAbstract Source # | |
Defined in Agda.Syntax.Common | |
LensIsAbstract MetaInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
LensIsAbstract TCEnv Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
LensIsAbstract (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info lensIsAbstract :: Lens' (DefInfo' t) IsAbstract Source # | |
LensIsAbstract (Closure a) Source # | |
Defined in Agda.TypeChecking.Monad.Base lensIsAbstract :: Lens' (Closure a) IsAbstract Source # |
class AnyIsAbstract a where Source #
Is any element of a collection an AbstractDef
.
Nothing
anyIsAbstract :: a -> IsAbstract Source #
default anyIsAbstract :: forall (t :: Type -> Type) b. (Foldable t, AnyIsAbstract b, t b ~ a) => a -> IsAbstract Source #
Instances
AnyIsAbstract IsAbstract Source # | |
Defined in Agda.Syntax.Common anyIsAbstract :: IsAbstract -> IsAbstract Source # | |
AnyIsAbstract (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info anyIsAbstract :: DefInfo' t -> IsAbstract Source # | |
AnyIsAbstract a => AnyIsAbstract (Maybe a) Source # | |
Defined in Agda.Syntax.Common anyIsAbstract :: Maybe a -> IsAbstract Source # | |
AnyIsAbstract a => AnyIsAbstract [a] Source # | |
Defined in Agda.Syntax.Common anyIsAbstract :: [a] -> IsAbstract Source # |
data IsInstance Source #
Is this definition eligible for instance search?
InstanceDef KwRange | Range of the |
NotInstanceDef |
Instances
HasRange IsInstance Source # | |
Defined in Agda.Syntax.Common getRange :: IsInstance -> Range Source # | |
KillRange IsInstance Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj IsInstance Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: IsInstance -> S Int32 Source # icod_ :: IsInstance -> S Int32 Source # value :: Int32 -> R IsInstance Source # | |
NFData IsInstance Source # | |
Defined in Agda.Syntax.Common rnf :: IsInstance -> () | |
Show IsInstance Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> IsInstance -> ShowS show :: IsInstance -> String showList :: [IsInstance] -> ShowS | |
Eq IsInstance Source # | |
Defined in Agda.Syntax.Common (==) :: IsInstance -> IsInstance -> Bool (/=) :: IsInstance -> IsInstance -> Bool | |
Ord IsInstance Source # | |
Defined in Agda.Syntax.Common compare :: IsInstance -> IsInstance -> Ordering (<) :: IsInstance -> IsInstance -> Bool (<=) :: IsInstance -> IsInstance -> Bool (>) :: IsInstance -> IsInstance -> Bool (>=) :: IsInstance -> IsInstance -> Bool max :: IsInstance -> IsInstance -> IsInstance min :: IsInstance -> IsInstance -> IsInstance |
Is this a macro definition?
Instances
HasRange IsMacro Source # | |||||
KillRange IsMacro Source # | |||||
Defined in Agda.Syntax.Common | |||||
NFData IsMacro Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic IsMacro Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show IsMacro Source # | |||||
Eq IsMacro Source # | |||||
Ord IsMacro Source # | |||||
type Rep IsMacro Source # | |||||
Defined in Agda.Syntax.Common type Rep IsMacro = D1 ('MetaData "IsMacro" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "MacroDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotMacroDef" 'PrefixI 'False) (U1 :: Type -> Type)) |
The unique identifier of an opaque block. Second argument is the top-level module identifier.
OpaqueId !Word64 !ModuleNameHash |
Instances
Pretty OpaqueId Source # | |||||
KillRange OpaqueId Source # | |||||
Defined in Agda.Syntax.Common | |||||
HasFresh OpaqueId Source # | |||||
EmbPrj OpaqueId Source # | |||||
NFData OpaqueId Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum OpaqueId Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic OpaqueId Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show OpaqueId Source # | |||||
Eq OpaqueId Source # | |||||
Ord OpaqueId Source # | |||||
Hashable OpaqueId Source # | |||||
Defined in Agda.Syntax.Common hashWithSalt :: Int -> OpaqueId -> Int | |||||
type Rep OpaqueId Source # | |||||
Defined in Agda.Syntax.Common type Rep OpaqueId = D1 ('MetaData "OpaqueId" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "OpaqueId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash))) |
class LensIsOpaque a where Source #
lensIsOpaque :: Lens' a IsOpaque Source #
Instances
LensIsOpaque IsOpaque Source # | |
Defined in Agda.Syntax.Common | |
LensIsOpaque TCEnv Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
LensIsOpaque (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info |
data JointOpacity Source #
Monoid representing the combined opaque blocks of a Foldable
containing possibly-opaque declarations.
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. |
Instances
Monoid JointOpacity Source # | |
Defined in Agda.Syntax.Common mappend :: JointOpacity -> JointOpacity -> JointOpacity mconcat :: [JointOpacity] -> JointOpacity | |
Semigroup JointOpacity Source # | |
Defined in Agda.Syntax.Common (<>) :: JointOpacity -> JointOpacity -> JointOpacity # sconcat :: NonEmpty JointOpacity -> JointOpacity stimes :: Integral b => b -> JointOpacity -> JointOpacity |
class AllAreOpaque a where Source #
Nothing
jointOpacity :: a -> JointOpacity Source #
default jointOpacity :: forall (t :: Type -> Type) b. (Foldable t, AllAreOpaque b, t b ~ a) => a -> JointOpacity Source #
Instances
AllAreOpaque IsOpaque Source # | |
Defined in Agda.Syntax.Common jointOpacity :: IsOpaque -> JointOpacity Source # | |
AllAreOpaque (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info jointOpacity :: DefInfo' t -> JointOpacity Source # | |
AllAreOpaque a => AllAreOpaque (Maybe a) Source # | |
Defined in Agda.Syntax.Common jointOpacity :: Maybe a -> JointOpacity Source # | |
AllAreOpaque a => AllAreOpaque [a] Source # | |
Defined in Agda.Syntax.Common jointOpacity :: [a] -> JointOpacity Source # |
data PositionInName Source #
The position of a name part or underscore in a name.
Beginning | The following underscore is at the beginning of the name:
|
Middle | The following underscore is in the middle of the name:
|
End | The following underscore is at the end of the name: |
Instances
Show PositionInName Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> PositionInName -> ShowS show :: PositionInName -> String showList :: [PositionInName] -> ShowS | |
Eq PositionInName Source # | |
Defined in Agda.Syntax.Common (==) :: PositionInName -> PositionInName -> Bool (/=) :: PositionInName -> PositionInName -> Bool | |
Ord PositionInName Source # | |
Defined in Agda.Syntax.Common compare :: PositionInName -> PositionInName -> Ordering (<) :: PositionInName -> PositionInName -> Bool (<=) :: PositionInName -> PositionInName -> Bool (>) :: PositionInName -> PositionInName -> Bool (>=) :: PositionInName -> PositionInName -> Bool max :: PositionInName -> PositionInName -> PositionInName min :: PositionInName -> PositionInName -> PositionInName |
data MaybePlaceholder e Source #
Placeholders are used to represent the underscores in a section.
Placeholder !PositionInName | |
NoPlaceholder !(Maybe PositionInName) e | The second argument is used only (but not always) for name parts other than underscores. |
Instances
Functor MaybePlaceholder Source # | |
Defined in Agda.Syntax.Common fmap :: (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b (<$) :: a -> MaybePlaceholder b -> MaybePlaceholder a # | |
Foldable MaybePlaceholder Source # | |
Defined in Agda.Syntax.Common fold :: Monoid m => MaybePlaceholder m -> m foldMap :: Monoid m => (a -> m) -> MaybePlaceholder a -> m foldMap' :: Monoid m => (a -> m) -> MaybePlaceholder a -> m foldr :: (a -> b -> b) -> b -> MaybePlaceholder a -> b foldr' :: (a -> b -> b) -> b -> MaybePlaceholder a -> b foldl :: (b -> a -> b) -> b -> MaybePlaceholder a -> b foldl' :: (b -> a -> b) -> b -> MaybePlaceholder a -> b foldr1 :: (a -> a -> a) -> MaybePlaceholder a -> a foldl1 :: (a -> a -> a) -> MaybePlaceholder a -> a toList :: MaybePlaceholder a -> [a] null :: MaybePlaceholder a -> Bool length :: MaybePlaceholder a -> Int elem :: Eq a => a -> MaybePlaceholder a -> Bool maximum :: Ord a => MaybePlaceholder a -> a minimum :: Ord a => MaybePlaceholder a -> a sum :: Num a => MaybePlaceholder a -> a product :: Num a => MaybePlaceholder a -> a | |
Traversable MaybePlaceholder Source # | |
Defined in Agda.Syntax.Common traverse :: Applicative f => (a -> f b) -> MaybePlaceholder a -> f (MaybePlaceholder b) sequenceA :: Applicative f => MaybePlaceholder (f a) -> f (MaybePlaceholder a) mapM :: Monad m => (a -> m b) -> MaybePlaceholder a -> m (MaybePlaceholder b) sequence :: Monad m => MaybePlaceholder (m a) -> m (MaybePlaceholder a) | |
Pretty a => Pretty (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Concrete.Pretty pretty :: MaybePlaceholder a -> Doc Source # prettyPrec :: Int -> MaybePlaceholder a -> Doc Source # prettyList :: [MaybePlaceholder a] -> Doc Source # | |
ExprLike a => ExprLike (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Concrete.Generic mapExpr :: (Expr -> Expr) -> MaybePlaceholder a -> MaybePlaceholder a Source # foldExpr :: Monoid m => (Expr -> m) -> MaybePlaceholder a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> MaybePlaceholder a -> m (MaybePlaceholder a) Source # | |
HasRange a => HasRange (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Common getRange :: MaybePlaceholder a -> Range Source # | |
KillRange a => KillRange (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Common killRange :: KillRangeT (MaybePlaceholder a) Source # | |
NFData a => NFData (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Common rnf :: MaybePlaceholder a -> () | |
Show e => Show (MaybePlaceholder e) Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> MaybePlaceholder e -> ShowS show :: MaybePlaceholder e -> String showList :: [MaybePlaceholder e] -> ShowS | |
Eq e => Eq (MaybePlaceholder e) Source # | |
Defined in Agda.Syntax.Common (==) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool (/=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool | |
Ord e => Ord (MaybePlaceholder e) Source # | |
Defined in Agda.Syntax.Common compare :: MaybePlaceholder e -> MaybePlaceholder e -> Ordering (<) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool (<=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool (>) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool (>=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool max :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e min :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e |
noPlaceholder :: e -> MaybePlaceholder e Source #
An abbreviation: noPlaceholder =
.NoPlaceholder
Nothing
type PrecedenceLevel = Double Source #
Precedence levels for operators.
data FixityLevel Source #
Unrelated | No fixity declared. |
Related !PrecedenceLevel | Fixity level declared as the number. |
Instances
Pretty FixityLevel Source # | |
Defined in Agda.Syntax.Concrete.Pretty pretty :: FixityLevel -> Doc Source # prettyPrec :: Int -> FixityLevel -> Doc Source # prettyList :: [FixityLevel] -> Doc Source # | |
ToTerm FixityLevel Source # | |
Defined in Agda.TypeChecking.Primitive | |
EmbPrj FixityLevel Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: FixityLevel -> S Int32 Source # icod_ :: FixityLevel -> S Int32 Source # value :: Int32 -> R FixityLevel Source # | |
Null FixityLevel Source # | |
Defined in Agda.Syntax.Common empty :: FixityLevel Source # null :: FixityLevel -> Bool Source # | |
NFData FixityLevel Source # | |
Defined in Agda.Syntax.Common rnf :: FixityLevel -> () | |
Show FixityLevel Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> FixityLevel -> ShowS show :: FixityLevel -> String showList :: [FixityLevel] -> ShowS | |
Eq FixityLevel Source # | |
Defined in Agda.Syntax.Common (==) :: FixityLevel -> FixityLevel -> Bool (/=) :: FixityLevel -> FixityLevel -> Bool | |
Ord FixityLevel Source # | |
Defined in Agda.Syntax.Common compare :: FixityLevel -> FixityLevel -> Ordering (<) :: FixityLevel -> FixityLevel -> Bool (<=) :: FixityLevel -> FixityLevel -> Bool (>) :: FixityLevel -> FixityLevel -> Bool (>=) :: FixityLevel -> FixityLevel -> Bool max :: FixityLevel -> FixityLevel -> FixityLevel min :: FixityLevel -> FixityLevel -> FixityLevel |
The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.
Fixity' | |
|
Instances
LensFixity Fixity' Source # | |
Defined in Agda.Syntax.Common | |
LensFixity' Fixity' Source # | |
Defined in Agda.Syntax.Common | |
Pretty Fixity' Source # | |
KillRange Fixity' Source # | |
Defined in Agda.Syntax.Common | |
PrimTerm Fixity' Source # | |
PrimType Fixity' Source # | |
ToTerm Fixity' Source # | |
EmbPrj Fixity' Source # | |
Null Fixity' Source # | |
NFData Fixity' Source # | |
Defined in Agda.Syntax.Common | |
Show Fixity' Source # | |
Eq Fixity' Source # | |
class LensFixity a where Source #
lensFixity :: Lens' a Fixity Source #
Instances
LensFixity Name Source # | |
Defined in Agda.Syntax.Abstract.Name | |
LensFixity QName Source # | |
Defined in Agda.Syntax.Abstract.Name | |
LensFixity Fixity Source # | |
Defined in Agda.Syntax.Common | |
LensFixity Fixity' Source # | |
Defined in Agda.Syntax.Common | |
LensFixity NewNotation Source # | |
Defined in Agda.Syntax.Notation | |
LensFixity AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base | |
LensFixity (ThingWithFixity a) Source # | |
Defined in Agda.Syntax.Fixity lensFixity :: Lens' (ThingWithFixity a) Fixity Source # |
class LensFixity' a where Source #
lensFixity' :: Lens' a Fixity' Source #
Instances
LensFixity' Name Source # | |
Defined in Agda.Syntax.Abstract.Name | |
LensFixity' QName Source # | |
Defined in Agda.Syntax.Abstract.Name | |
LensFixity' Fixity' Source # | |
Defined in Agda.Syntax.Common | |
LensFixity' (ThingWithFixity a) Source # | |
Defined in Agda.Syntax.Fixity lensFixity' :: Lens' (ThingWithFixity a) Fixity' Source # |
type HidingDirective' n m = [ImportedName' n m] Source #
type RenamingDirective' n m = [Renaming' n m] Source #
defaultImportDir :: ImportDirective' n m Source #
Default is directive is private
(use everything, but do not export).
isDefaultImportDir :: ImportDirective' n m -> Bool Source #
isDefaultImportDir
implies null
, but not the other way round.
mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2 Source #
setImportedName :: ImportedName' a a -> a -> ImportedName' a a Source #
data PositivityCheck Source #
Positivity check? (Default = True).
Instances
KillRange PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
NFData PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common rnf :: PositivityCheck -> () | |||||
Monoid PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
Semigroup PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common (<>) :: PositivityCheck -> PositivityCheck -> PositivityCheck # sconcat :: NonEmpty PositivityCheck -> PositivityCheck stimes :: Integral b => b -> PositivityCheck -> PositivityCheck | |||||
Bounded PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common succ :: PositivityCheck -> PositivityCheck pred :: PositivityCheck -> PositivityCheck toEnum :: Int -> PositivityCheck fromEnum :: PositivityCheck -> Int enumFrom :: PositivityCheck -> [PositivityCheck] enumFromThen :: PositivityCheck -> PositivityCheck -> [PositivityCheck] enumFromTo :: PositivityCheck -> PositivityCheck -> [PositivityCheck] enumFromThenTo :: PositivityCheck -> PositivityCheck -> PositivityCheck -> [PositivityCheck] | |||||
Generic PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common
from :: PositivityCheck -> Rep PositivityCheck x to :: Rep PositivityCheck x -> PositivityCheck | |||||
Show PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> PositivityCheck -> ShowS show :: PositivityCheck -> String showList :: [PositivityCheck] -> ShowS | |||||
Eq PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common (==) :: PositivityCheck -> PositivityCheck -> Bool (/=) :: PositivityCheck -> PositivityCheck -> Bool | |||||
Ord PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common compare :: PositivityCheck -> PositivityCheck -> Ordering (<) :: PositivityCheck -> PositivityCheck -> Bool (<=) :: PositivityCheck -> PositivityCheck -> Bool (>) :: PositivityCheck -> PositivityCheck -> Bool (>=) :: PositivityCheck -> PositivityCheck -> Bool max :: PositivityCheck -> PositivityCheck -> PositivityCheck min :: PositivityCheck -> PositivityCheck -> PositivityCheck | |||||
type Rep PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common type Rep PositivityCheck = D1 ('MetaData "PositivityCheck" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "YesPositivityCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoPositivityCheck" 'PrefixI 'False) (U1 :: Type -> Type)) |
data UniverseCheck Source #
Universe check? (Default is yes).
Instances
KillRange UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
NFData UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common rnf :: UniverseCheck -> () | |||||
Bounded UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common succ :: UniverseCheck -> UniverseCheck pred :: UniverseCheck -> UniverseCheck toEnum :: Int -> UniverseCheck fromEnum :: UniverseCheck -> Int enumFrom :: UniverseCheck -> [UniverseCheck] enumFromThen :: UniverseCheck -> UniverseCheck -> [UniverseCheck] enumFromTo :: UniverseCheck -> UniverseCheck -> [UniverseCheck] enumFromThenTo :: UniverseCheck -> UniverseCheck -> UniverseCheck -> [UniverseCheck] | |||||
Generic UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common
from :: UniverseCheck -> Rep UniverseCheck x to :: Rep UniverseCheck x -> UniverseCheck | |||||
Show UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> UniverseCheck -> ShowS show :: UniverseCheck -> String showList :: [UniverseCheck] -> ShowS | |||||
Eq UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common (==) :: UniverseCheck -> UniverseCheck -> Bool (/=) :: UniverseCheck -> UniverseCheck -> Bool | |||||
Ord UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common compare :: UniverseCheck -> UniverseCheck -> Ordering (<) :: UniverseCheck -> UniverseCheck -> Bool (<=) :: UniverseCheck -> UniverseCheck -> Bool (>) :: UniverseCheck -> UniverseCheck -> Bool (>=) :: UniverseCheck -> UniverseCheck -> Bool max :: UniverseCheck -> UniverseCheck -> UniverseCheck min :: UniverseCheck -> UniverseCheck -> UniverseCheck | |||||
type Rep UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common type Rep UniverseCheck = D1 ('MetaData "UniverseCheck" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "YesUniverseCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoUniverseCheck" 'PrefixI 'False) (U1 :: Type -> Type)) |
data CoverageCheck Source #
Coverage check? (Default is yes).
Instances
KillRange CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
NFData CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common rnf :: CoverageCheck -> () | |||||
Monoid CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common mappend :: CoverageCheck -> CoverageCheck -> CoverageCheck mconcat :: [CoverageCheck] -> CoverageCheck | |||||
Semigroup CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common (<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck # sconcat :: NonEmpty CoverageCheck -> CoverageCheck stimes :: Integral b => b -> CoverageCheck -> CoverageCheck | |||||
Bounded CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common succ :: CoverageCheck -> CoverageCheck pred :: CoverageCheck -> CoverageCheck toEnum :: Int -> CoverageCheck fromEnum :: CoverageCheck -> Int enumFrom :: CoverageCheck -> [CoverageCheck] enumFromThen :: CoverageCheck -> CoverageCheck -> [CoverageCheck] enumFromTo :: CoverageCheck -> CoverageCheck -> [CoverageCheck] enumFromThenTo :: CoverageCheck -> CoverageCheck -> CoverageCheck -> [CoverageCheck] | |||||
Generic CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common
from :: CoverageCheck -> Rep CoverageCheck x to :: Rep CoverageCheck x -> CoverageCheck | |||||
Show CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common showsPrec :: Int -> CoverageCheck -> ShowS show :: CoverageCheck -> String showList :: [CoverageCheck] -> ShowS | |||||
Eq CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common (==) :: CoverageCheck -> CoverageCheck -> Bool (/=) :: CoverageCheck -> CoverageCheck -> Bool | |||||
Ord CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common compare :: CoverageCheck -> CoverageCheck -> Ordering (<) :: CoverageCheck -> CoverageCheck -> Bool (<=) :: CoverageCheck -> CoverageCheck -> Bool (>) :: CoverageCheck -> CoverageCheck -> Bool (>=) :: CoverageCheck -> CoverageCheck -> Bool max :: CoverageCheck -> CoverageCheck -> CoverageCheck min :: CoverageCheck -> CoverageCheck -> CoverageCheck | |||||
type Rep CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common type Rep CoverageCheck = D1 ('MetaData "CoverageCheck" "Agda.Syntax.Common" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "YesCoverageCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoCoverageCheck" 'PrefixI 'False) (U1 :: Type -> Type)) |
data ExpandedEllipsis Source #
Instances
KillRange ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj ExpandedEllipsis Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: ExpandedEllipsis -> S Int32 Source # icod_ :: ExpandedEllipsis -> S Int32 Source # value :: Int32 -> R ExpandedEllipsis Source # | |
Null ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common empty :: ExpandedEllipsis Source # null :: ExpandedEllipsis -> Bool Source # | |
NFData ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common rnf :: ExpandedEllipsis -> () | |
Monoid ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common | |
Semigroup ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common (<>) :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis # sconcat :: NonEmpty ExpandedEllipsis -> ExpandedEllipsis stimes :: Integral b => b -> ExpandedEllipsis -> ExpandedEllipsis | |
Show ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> ExpandedEllipsis -> ShowS show :: ExpandedEllipsis -> String showList :: [ExpandedEllipsis] -> ShowS | |
Eq ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common (==) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool (/=) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool |
data NotationPart Source #
Notation parts.
IdPart RString | An identifier part. For instance, for |
HolePart Range (NamedArg (Ranged Int)) | A hole: a place where argument expressions can be written.
For instance, for |
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). |
Instances
Pretty NotationPart Source # | |
Defined in Agda.Syntax.Concrete.Pretty pretty :: NotationPart -> Doc Source # prettyPrec :: Int -> NotationPart -> Doc Source # prettyList :: [NotationPart] -> Doc Source # | |
HasRange NotationPart Source # | |
Defined in Agda.Syntax.Common getRange :: NotationPart -> Range Source # | |
KillRange NotationPart Source # | |
Defined in Agda.Syntax.Common | |
SetRange NotationPart Source # | |
Defined in Agda.Syntax.Common setRange :: Range -> NotationPart -> NotationPart Source # | |
EmbPrj NotationPart Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: NotationPart -> S Int32 Source # icod_ :: NotationPart -> S Int32 Source # value :: Int32 -> R NotationPart Source # | |
NFData NotationPart Source # | |
Defined in Agda.Syntax.Common rnf :: NotationPart -> () | |
Show NotationPart Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> NotationPart -> ShowS show :: NotationPart -> String showList :: [NotationPart] -> ShowS | |
Eq NotationPart Source # | |
Defined in Agda.Syntax.Common (==) :: NotationPart -> NotationPart -> Bool (/=) :: NotationPart -> NotationPart -> Bool | |
Ord NotationPart Source # | |
Defined in Agda.Syntax.Common compare :: NotationPart -> NotationPart -> Ordering (<) :: NotationPart -> NotationPart -> Bool (<=) :: NotationPart -> NotationPart -> Bool (>) :: NotationPart -> NotationPart -> Bool (>=) :: NotationPart -> NotationPart -> Bool max :: NotationPart -> NotationPart -> NotationPart min :: NotationPart -> NotationPart -> NotationPart |
data BoundVariablePosition Source #
Positions of variables in syntax declarations.
BoundVariablePosition | |
|
Instances
EmbPrj BoundVariablePosition Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common icode :: BoundVariablePosition -> S Int32 Source # icod_ :: BoundVariablePosition -> S Int32 Source # value :: Int32 -> R BoundVariablePosition Source # | |
NFData BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common rnf :: BoundVariablePosition -> () | |
Show BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common showsPrec :: Int -> BoundVariablePosition -> ShowS show :: BoundVariablePosition -> String showList :: [BoundVariablePosition] -> ShowS | |
Eq BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common (==) :: BoundVariablePosition -> BoundVariablePosition -> Bool (/=) :: BoundVariablePosition -> BoundVariablePosition -> Bool | |
Ord BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common compare :: BoundVariablePosition -> BoundVariablePosition -> Ordering (<) :: BoundVariablePosition -> BoundVariablePosition -> Bool (<=) :: BoundVariablePosition -> BoundVariablePosition -> Bool (>) :: BoundVariablePosition -> BoundVariablePosition -> Bool (>=) :: BoundVariablePosition -> BoundVariablePosition -> Bool max :: BoundVariablePosition -> BoundVariablePosition -> BoundVariablePosition min :: BoundVariablePosition -> BoundVariablePosition -> BoundVariablePosition |
Instances
PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common patternMatchingAllowed :: Induction -> Bool Source # | |
Pretty Induction Source # | |
HasRange Induction Source # | |
KillRange Induction Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Induction Source # | |
NFData Induction Source # | |
Defined in Agda.Syntax.Common.Aspect | |
Show Induction Source # | |
Eq Induction Source # | |
Ord Induction Source # | |
Defined in Agda.Syntax.Common.Aspect |