| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Common
Contents
Description
Some common syntactic entities are defined in this module.
Synopsis
- type Arity = Nat
- data OverlapMode
- data Overlappable
- type Nat = Int
- data Associativity
- data Fixity = Fixity {}
- newtype Constr a = Constr a
- data Arg e = Arg {}
- hidden :: LensHiding a => a -> Bool
- data Origin
- data FileType
- data Lock
- data PositionInName
- data ImportDirective' n m = ImportDirective {
- importDirRange :: Range
- using :: Using' n m
- hiding :: HidingDirective' n m
- impRenaming :: RenamingDirective' n m
- publicOpen :: Maybe KwRange
- isInstance :: LensHiding a => a -> Bool
- defaultFixity :: Fixity
- data Q1Origin
- = Q1Inferred
- | Q1 Range
- | Q1Linear Range
- class LensLock a where
- data IsMain
- type BackendName = Text
- newtype InteractionId = InteractionId {
- interactionId :: Nat
- data Modality = Modality {}
- newtype ProblemId = ProblemId Nat
- data RewriteEqn' qn nm p e
- data MetaId = MetaId {
- metaId :: !Word64
- metaModule :: !ModuleNameHash
- data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
- data ConstructorOrPatternSynonym
- 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 :: 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 ExprKind
- data Cubical
- data Language
- type NamedArg a = Arg (Named_ a)
- class LensArgInfo a where
- getArgInfo :: a -> ArgInfo
- setArgInfo :: ArgInfo -> a -> a
- mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a
- class LensCohesion a where
- getCohesion :: a -> Cohesion
- setCohesion :: Cohesion -> a -> a
- mapCohesion :: (Cohesion -> Cohesion) -> a -> a
- class LensModality a where
- getModality :: a -> Modality
- setModality :: Modality -> a -> a
- mapModality :: (Modality -> Modality) -> a -> a
- class LensQuantity a where
- getQuantity :: a -> Quantity
- setQuantity :: Quantity -> a -> a
- mapQuantity :: (Quantity -> Quantity) -> a -> a
- class LensRelevance a where
- getRelevance :: a -> Relevance
- setRelevance :: Relevance -> a -> a
- mapRelevance :: (Relevance -> Relevance) -> a -> a
- class LensModalPolarity a where
- getModalPolarity :: a -> PolarityModality
- setModalPolarity :: PolarityModality -> a -> a
- mapModalPolarity :: (PolarityModality -> PolarityModality) -> a -> a
- fromImportedName :: ImportedName' a a -> a
- partitionImportedNames :: [ImportedName' n m] -> ([n], [m])
- data IsOpaque
- irrelevant :: Relevance
- relevant :: Relevance
- hasQuantity0 :: LensQuantity a => a -> Bool
- data WithHiding a = WithHiding {}
- data PolarityModality = PolarityModality {}
- data Relevance
- type Nat1 = Nat
- cubicalOptionString :: Cubical -> String
- data DisplayLHS
- type HasEta0 = HasEta' ()
- emptyRecordDirectives :: Null a => 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
- mergeHiding :: LensHiding a => WithHiding a -> a
- notVisible :: 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
- prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
- 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
- usableRelevance :: LensRelevance a => a -> Bool
- usableQuantity :: LensQuantity a => a -> Bool
- usableCohesion :: LensCohesion a => a -> Bool
- usablePolarity :: LensModalPolarity a => a -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- composeQuantity :: Quantity -> Quantity -> Quantity
- composeCohesion :: Cohesion -> Cohesion -> Cohesion
- composePolarity :: PolarityModality -> PolarityModality -> PolarityModality
- applyModality :: LensModality a => Modality -> a -> a
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- inverseComposeQuantity :: Quantity -> Quantity -> Quantity
- inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion
- inverseComposePolarity :: PolarityModality -> PolarityModality -> PolarityModality
- inverseApplyModalityButNotQuantity :: LensModality a => Modality -> a -> a
- addRelevance :: Relevance -> Relevance -> Relevance
- addQuantity :: Quantity -> Quantity -> Quantity
- addCohesion :: Cohesion -> Cohesion -> Cohesion
- addPolarity :: PolarityModality -> PolarityModality -> PolarityModality
- zeroRelevance :: Relevance
- zeroQuantity :: Quantity
- zeroCohesion :: Cohesion
- zeroPolarity :: PolarityModality
- unitRelevance :: Relevance
- unitQuantity :: Quantity
- unitCohesion :: Cohesion
- unitPolarity :: PolarityModality
- topModality :: Modality
- topRelevance :: Relevance
- topQuantity :: Quantity
- topCohesion :: Cohesion
- topPolarity :: PolarityModality
- defaultModality :: Modality
- defaultRelevance :: Relevance
- defaultQuantity :: Quantity
- defaultCohesion :: Cohesion
- defaultPolarity :: PolarityModality
- defaultCheckModality :: Modality
- withStandardLock :: ModalPolarity -> PolarityModality
- data ModalPolarity
- positionalModalityComponent :: Modality -> Modality
- sameModality :: (LensModality a, LensModality b) => a -> b -> Bool
- sameRelevance :: Relevance -> Relevance -> Bool
- sameQuantity :: Quantity -> Quantity -> Bool
- sameCohesion :: Cohesion -> Cohesion -> Bool
- samePolarity :: PolarityModality -> PolarityModality -> Bool
- lModRelevance :: Lens' Modality Relevance
- lModQuantity :: Lens' Modality Quantity
- lModCohesion :: Lens' Modality Cohesion
- lModPolarity :: Lens' Modality PolarityModality
- 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
- getPolarityMod :: LensModality a => LensGet a PolarityModality
- setPolarityMod :: LensModality a => LensSet a PolarityModality
- mapPolarityMod :: LensModality a => LensMap a PolarityModality
- 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
- isQuantity0 :: LensQuantity a => a -> Bool
- isQuantityω :: LensQuantity a => a -> Bool
- prettyQuantity :: LensQuantity a => a -> Doc -> Doc
- data Erased
- defaultErased :: Erased
- asQuantity :: Erased -> Quantity
- erasedFromQuantity :: Quantity -> Maybe Erased
- sameErased :: Erased -> Erased -> Bool
- isErased :: Erased -> Bool
- composeErased :: Erased -> Erased -> Erased
- prettyErased :: Erased -> Doc -> Doc
- data OriginRelevant
- data OriginIrrelevant
- data OriginShapeIrrelevant
- shapeIrrelevant :: Relevance
- isRelevant :: LensRelevance a => a -> Bool
- isIrrelevant :: LensRelevance a => a -> Bool
- isShapeIrrelevant :: LensRelevance a => a -> Bool
- moreRelevant :: Relevance -> Relevance -> Bool
- applyRelevance :: LensRelevance a => Relevance -> a -> a
- inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a
- irrelevantToShapeIrrelevant :: Relevance -> Relevance
- shapeIrrelevantToRelevant :: Relevance -> Relevance
- shapeIrrelevantToIrrelevant :: Relevance -> Relevance
- prettyRelevance :: LensRelevance a => a -> Doc -> Doc
- 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
- prettyLock :: LensLock a => a -> Doc -> Doc
- allCohesions :: [Cohesion]
- isContinuous :: LensCohesion a => a -> Bool
- moreCohesion :: Cohesion -> Cohesion -> Bool
- applyCohesion :: LensCohesion a => Cohesion -> a -> a
- inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a
- prettyCohesion :: LensCohesion a => a -> Doc -> Doc
- allModalPolarities :: [ModalPolarity]
- morePolarity' :: ModalPolarity -> ModalPolarity -> Bool
- splittablePolarity :: LensModalPolarity a => a -> Bool
- composePolarity' :: ModalPolarity -> ModalPolarity -> ModalPolarity
- inverseComposePolarity' :: ModalPolarity -> ModalPolarity -> ModalPolarity
- addPolarity' :: ModalPolarity -> ModalPolarity -> ModalPolarity
- morePolarity :: PolarityModality -> PolarityModality -> Bool
- applyPolarity :: LensModalPolarity a => PolarityModality -> a -> a
- inverseApplyPolarity :: LensModalPolarity a => PolarityModality -> a -> a
- negativePolarity :: PolarityModality
- mixedPolarity :: PolarityModality
- prettyPolarity :: LensModalPolarity a => a -> Doc -> Doc
- data BinderNameOrigin
- data FreeVariables
- 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
- defaultIrrelevantArgInfo :: ArgInfo
- 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
- defaultArg :: a -> Arg a
- 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 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 Catchall
- data CoverageCheck
- data ExpandedEllipsis
- = ExpandedEllipsis { }
- | NoEllipsis
- data NotationPart
- data BoundVariablePosition = BoundVariablePosition {
- holeNumber :: !Int
- varNumber :: !Int
- module Agda.Syntax.Common.KeywordRange
- module Agda.Syntax.TopLevelModuleName.Boot
- data Induction
Documentation
data OverlapMode Source #
The possible overlap modes for an instance, also used for instance candidates.
Constructors
| Overlappable | User-written OVERLAPPABLE pragma: this candidate can *be removed* by a more specific candidate. |
| Overlapping | User-written OVERLAPPING pragma: this candidate can *remove* a less specific candidate. |
| Overlaps | User-written OVERLAPS pragma: both overlappable and overlapping. |
| DefaultOverlap | No user-written overlap pragma. This instance can be overlapped by an OVERLAPPING instance, and it can overlap OVERLAPPABLE instances. |
| Incoherent | User-written INCOHERENT pragma: both overlappable and overlapping; and, if there are multiple candidates after all overlap has been handled, make an arbitrary choice. |
| FieldOverlap | Overlapping instances in record fields. |
Instances
data Overlappable Source #
Constructors
| YesOverlap | |
| NoOverlap |
Instances
data Associativity Source #
Associativity.
Constructors
| NonAssoc | |
| LeftAssoc | |
| RightAssoc |
Instances
Fixity of operators.
Constructors
| Fixity | |
Fields
| |
Instances
| LensFixity Fixity Source # | |
Defined in Agda.Syntax.Common | |
| Pretty Fixity Source # | |
| HasRange Fixity Source # | |
| KillRange Fixity Source # | |
Defined in Agda.Syntax.Common Methods | |
| 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 # | |
Constructors
| Constr a |
Instances
| ToConcrete (Constr Constructor) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => Constr Constructor -> m (ConOfAbs (Constr Constructor)) Source # bindToConcrete :: MonadToConcrete m => Constr Constructor -> (ConOfAbs (Constr Constructor) -> m b) -> m b Source # | |||||
| type ConOfAbs (Constr Constructor) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
Instances
:: LensHiding a => a -> Bool Source #
Hidden arguments are hidden.
Origin of arguments.
Constructors
| UserWritten | From the source file / user input. (Preserve!) |
| Inserted | E.g. inserted hidden arguments. |
| Reflected | Produced by the reflection machinery. |
| CaseSplit | Produced by an interactive case split. |
| Substitution | Named application produced to represent a substitution. E.g. "?0 (x = n)" instead of "?0 n" |
| ExpandedPun | An expanded hidden argument pun. |
| Generalization | Inserted by the generalization process |
Instances
| LensOrigin Origin Source # | |
| HasRange Origin Source # | |
| KillRange Origin Source # | |
Defined in Agda.Syntax.Common Methods | |
| ChooseFlex Origin Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods 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 # | |
Instances
| Pretty FileType Source # | |||||
| EmbPrj FileType Source # | |||||
| NFData FileType Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic FileType Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show FileType Source # | |||||
| Eq FileType Source # | |||||
| Ord FileType Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type Rep FileType Source # | |||||
Defined in Agda.Syntax.Common type Rep FileType = D1 ('MetaData "FileType" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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) :+: C1 ('MetaCons "TreeFileType" 'PrefixI 'False) (U1 :: Type -> Type)))) | |||||
Constructors
| 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 # | |||||
| Null Lock Source # | |||||
| NFData Lock Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic Lock Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| 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.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) (C1 ('MetaCons "IsNotLock" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsLock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LockOrigin))) | |||||
data PositionInName Source #
The position of a name part or underscore in a name.
Constructors
| 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 | |
| Eq PositionInName Source # | |
Defined in Agda.Syntax.Common Methods (==) :: PositionInName -> PositionInName -> Bool Source # (/=) :: PositionInName -> PositionInName -> Bool Source # | |
| Ord PositionInName Source # | |
Defined in Agda.Syntax.Common Methods compare :: PositionInName -> PositionInName -> Ordering Source # (<) :: PositionInName -> PositionInName -> Bool Source # (<=) :: PositionInName -> PositionInName -> Bool Source # (>) :: PositionInName -> PositionInName -> Bool Source # (>=) :: PositionInName -> PositionInName -> Bool Source # max :: PositionInName -> PositionInName -> PositionInName Source # min :: PositionInName -> PositionInName -> PositionInName Source # | |
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).
Constructors
| ImportDirective | |
Fields
| |
Instances
| (Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # | |
Defined in Agda.Syntax.Common Methods pretty :: ImportDirective' a b -> Doc Source # prettyPrec :: Int -> ImportDirective' a b -> Doc Source # prettyList :: [ImportDirective' a b] -> Doc Source # | |
| (HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: ImportDirective' a b -> Range Source # | |
| (KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportDirective' a b) Source # | |
| Null (ImportDirective' n m) Source # |
|
Defined in Agda.Syntax.Common | |
| (NFData a, NFData b) => NFData (ImportDirective' a b) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common Methods rnf :: ImportDirective' a b -> () Source # | |
| (HasRange n, HasRange m) => Monoid (ImportDirective' n m) Source # | |
Defined in Agda.Syntax.Common Methods mempty :: ImportDirective' n m Source # mappend :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m Source # mconcat :: [ImportDirective' n m] -> ImportDirective' n m Source # | |
| (HasRange n, HasRange m) => Semigroup (ImportDirective' n m) Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m Source # sconcat :: NonEmpty (ImportDirective' n m) -> ImportDirective' n m Source # stimes :: Integral b => b -> ImportDirective' n m -> ImportDirective' n m Source # | |
| (Show m, Show n) => Show (ImportDirective' n m) Source # | |
Defined in Agda.Syntax.Common | |
| (Eq m, Eq n) => Eq (ImportDirective' n m) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: ImportDirective' n m -> ImportDirective' n m -> Bool Source # (/=) :: ImportDirective' n m -> ImportDirective' n m -> Bool Source # | |
isInstance :: LensHiding a => a -> Bool Source #
Origin of Quantity1.
Constructors
| 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 Methods | |||||
| 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 Associated Types
| |||||
| Show Q1Origin Source # | |||||
| Eq Q1Origin Source # | |||||
| Ord Q1Origin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type Rep Q1Origin Source # | |||||
Defined in Agda.Syntax.Common type Rep Q1Origin = D1 ('MetaData "Q1Origin" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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)))) | |||||
class LensLock a where Source #
Minimal complete definition
type BackendName = Text Source #
newtype InteractionId Source #
Constructors
| InteractionId | |
Fields
| |
Instances
| EncodeTCM InteractionId Source # | |||||
Defined in Agda.Interaction.JSONTop | |||||
| Pretty InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods pretty :: InteractionId -> Doc Source # prettyPrec :: Int -> InteractionId -> Doc Source # prettyList :: [InteractionId] -> Doc Source # | |||||
| KillRange InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| ToConcrete InteractionId Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => InteractionId -> m (ConOfAbs InteractionId) Source # bindToConcrete :: MonadToConcrete m => InteractionId -> (ConOfAbs InteractionId -> m b) -> m b Source # | |||||
| HasFresh InteractionId Source # | |||||
Defined in Agda.TypeChecking.Monad.Base | |||||
| PrettyTCM InteractionId Source # | |||||
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => InteractionId -> m Doc Source # | |||||
| ToJSON InteractionId Source # | |||||
Defined in Agda.Interaction.JSONTop Methods toJSON :: InteractionId -> Value Source # toEncoding :: InteractionId -> Encoding Source # toJSONList :: [InteractionId] -> Value Source # toEncodingList :: [InteractionId] -> Encoding Source # omitField :: InteractionId -> Bool Source # | |||||
| NFData InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: InteractionId -> () Source # | |||||
| NFData InteractionPoints Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: InteractionPoints -> () Source # | |||||
| Enum InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: InteractionId -> InteractionId Source # pred :: InteractionId -> InteractionId Source # toEnum :: Int -> InteractionId Source # fromEnum :: InteractionId -> Int Source # enumFrom :: InteractionId -> [InteractionId] Source # enumFromThen :: InteractionId -> InteractionId -> [InteractionId] Source # enumFromTo :: InteractionId -> InteractionId -> [InteractionId] Source # enumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId] Source # | |||||
| Num InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods (+) :: InteractionId -> InteractionId -> InteractionId Source # (-) :: InteractionId -> InteractionId -> InteractionId Source # (*) :: InteractionId -> InteractionId -> InteractionId Source # negate :: InteractionId -> InteractionId Source # abs :: InteractionId -> InteractionId Source # signum :: InteractionId -> InteractionId Source # fromInteger :: Integer -> InteractionId Source # | |||||
| Read InteractionId Source # | |||||
Defined in Agda.Interaction.Base | |||||
| Integral InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods quot :: InteractionId -> InteractionId -> InteractionId Source # rem :: InteractionId -> InteractionId -> InteractionId Source # div :: InteractionId -> InteractionId -> InteractionId Source # mod :: InteractionId -> InteractionId -> InteractionId Source # quotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId) Source # divMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId) Source # toInteger :: InteractionId -> Integer Source # | |||||
| Real InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods toRational :: InteractionId -> Rational Source # | |||||
| Show InteractionId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: InteractionId -> InteractionId -> Bool Source # (/=) :: InteractionId -> InteractionId -> Bool Source # | |||||
| Ord InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: InteractionId -> InteractionId -> Ordering Source # (<) :: InteractionId -> InteractionId -> Bool Source # (<=) :: InteractionId -> InteractionId -> Bool Source # (>) :: InteractionId -> InteractionId -> Bool Source # (>=) :: InteractionId -> InteractionId -> Bool Source # max :: InteractionId -> InteractionId -> InteractionId Source # min :: InteractionId -> InteractionId -> InteractionId Source # | |||||
| type ConOfAbs InteractionId Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
We have a tuple of modalities, which might not be fully orthogonal. For example, irrelevant stuff is also run-time irrelevant.
Constructors
| Modality | |
Fields
| |
Instances
| LensCohesion Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| LensModalPolarity Modality Source # | |||||
Defined in Agda.Syntax.Common Methods getModalPolarity :: Modality -> PolarityModality Source # setModalPolarity :: PolarityModality -> Modality -> Modality Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> Modality -> Modality Source # | |||||
| 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 Methods | |||||
| Verbalize Modality Source # | |||||
| PrettyTCM Modality Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| EmbPrj Modality Source # | |||||
| Unquote Modality Source # | |||||
| Null Modality Source # | |||||
| PartialOrd Modality Source # | Dominance ordering. | ||||
Defined in Agda.Syntax.Common Methods | |||||
| NFData Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic Modality Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Modality Source # | |||||
| Eq Modality Source # | |||||
| Ord Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| IsVarSet () AllowedVar Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Occurs Methods withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar Source # | |||||
| LeftClosedPOMonoid (UnderComposition Modality) Source # | |||||
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality Source # | |||||
| 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 Methods mempty :: UnderAddition Modality Source # mappend :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality Source # mconcat :: [UnderAddition Modality] -> UnderAddition Modality Source # | |||||
| Monoid (UnderComposition Modality) Source # | Pointwise composition unit. | ||||
Defined in Agda.Syntax.Common | |||||
| Semigroup (UnderAddition Modality) Source # | Pointwise addition. | ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality Source # sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality Source # stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality Source # | |||||
| Semigroup (UnderComposition Modality) Source # | Pointwise composition. | ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality Source # sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality Source # stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality Source # | |||||
| type Rep Modality Source # | |||||
Defined in Agda.Syntax.Common type Rep Modality = D1 ('MetaData "Modality" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) (C1 ('MetaCons "Modality" 'PrefixI 'True) ((S1 ('MetaSel ('Just "modRelevance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Relevance) :*: S1 ('MetaSel ('Just "modQuantity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Quantity)) :*: (S1 ('MetaSel ('Just "modCohesion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cohesion) :*: S1 ('MetaSel ('Just "modPolarity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PolarityModality)))) | |||||
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 # | |
| ToJSON ProblemId Source # | |
| NFData ProblemId Source # | |
Defined in Agda.Syntax.Common | |
| Enum ProblemId Source # | |
Defined in Agda.Syntax.Common Methods succ :: ProblemId -> ProblemId Source # pred :: ProblemId -> ProblemId Source # toEnum :: Int -> ProblemId Source # fromEnum :: ProblemId -> Int Source # enumFrom :: ProblemId -> [ProblemId] Source # enumFromThen :: ProblemId -> ProblemId -> [ProblemId] Source # enumFromTo :: ProblemId -> ProblemId -> [ProblemId] Source # enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId] Source # | |
| Num ProblemId Source # | |
Defined in Agda.Syntax.Common Methods (+) :: ProblemId -> ProblemId -> ProblemId Source # (-) :: ProblemId -> ProblemId -> ProblemId Source # (*) :: ProblemId -> ProblemId -> ProblemId Source # negate :: ProblemId -> ProblemId Source # abs :: ProblemId -> ProblemId Source # signum :: ProblemId -> ProblemId Source # fromInteger :: Integer -> ProblemId Source # | |
| Integral ProblemId Source # | |
Defined in Agda.Syntax.Common Methods quot :: ProblemId -> ProblemId -> ProblemId Source # rem :: ProblemId -> ProblemId -> ProblemId Source # div :: ProblemId -> ProblemId -> ProblemId Source # mod :: ProblemId -> ProblemId -> ProblemId Source # quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId) Source # divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId) Source # | |
| Real ProblemId Source # | |
Defined in Agda.Syntax.Common Methods toRational :: ProblemId -> Rational Source # | |
| Show ProblemId Source # | |
| Eq ProblemId Source # | |
| Ord ProblemId Source # | |
Defined in Agda.Syntax.Common | |
| Monad m => MonadFresh ProblemId (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m ProblemId 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
Constructors
| Rewrite (List1 (qn, e)) | rewrite e |
| Invert qn (List1 (Named nm (p, e))) | with p <- e in eq |
| LeftLet (List1 (p, e)) | using p <- e |
Instances
| ToAbstract RewriteEqn Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source # | |||||
| Functor (RewriteEqn' qn nm p) Source # | |||||
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> RewriteEqn' qn nm p a -> RewriteEqn' qn nm p b Source # (<$) :: a -> RewriteEqn' qn nm p b -> RewriteEqn' qn nm p a Source # | |||||
| Foldable (RewriteEqn' qn nm p) Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => RewriteEqn' qn nm p m -> m Source # foldMap :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m Source # foldMap' :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m Source # foldr :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b Source # foldr' :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b Source # foldl :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b Source # foldl' :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b Source # foldr1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a Source # foldl1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a Source # toList :: RewriteEqn' qn nm p a -> [a] Source # null :: RewriteEqn' qn nm p a -> Bool Source # length :: RewriteEqn' qn nm p a -> Int Source # elem :: Eq a => a -> RewriteEqn' qn nm p a -> Bool Source # maximum :: Ord a => RewriteEqn' qn nm p a -> a Source # minimum :: Ord a => RewriteEqn' qn nm p a -> a Source # sum :: Num a => RewriteEqn' qn nm p a -> a Source # product :: Num a => RewriteEqn' qn nm p a -> a Source # | |||||
| Traversable (RewriteEqn' qn nm p) Source # | |||||
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> RewriteEqn' qn nm p a -> f (RewriteEqn' qn nm p b) Source # sequenceA :: Applicative f => RewriteEqn' qn nm p (f a) -> f (RewriteEqn' qn nm p a) Source # mapM :: Monad m => (a -> m b) -> RewriteEqn' qn nm p a -> m (RewriteEqn' qn nm p b) Source # sequence :: Monad m => RewriteEqn' qn nm p (m a) -> m (RewriteEqn' qn nm p a) Source # | |||||
| (ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods 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 Methods 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 Methods 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 Methods 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 Methods 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 Associated Types
Methods toConcrete :: MonadToConcrete m => RewriteEqn' qn BindName p a -> m (ConOfAbs (RewriteEqn' qn BindName p a)) Source # bindToConcrete :: MonadToConcrete m => RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> m b) -> m b Source # | |||||
| ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types
Methods 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 Methods rnf :: RewriteEqn' qn nm p e -> () Source # | |||||
| (Show e, Show qn, Show nm, Show p) => Show (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| (Eq e, Eq qn, Eq nm, Eq p) => Eq (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool Source # (/=) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool Source # | |||||
| 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 NameIds.
Constructors
| MetaId | |
Fields
| |
Instances
| EncodeTCM MetaId Source # | |||||
| Pretty MetaId Source # | |||||
| GetDefs MetaId Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => MetaId -> m () Source # | |||||
| NamesIn MetaId Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
| Reify MetaId Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
| HasFresh MetaId Source # | |||||
| IsInstantiatedMeta MetaId Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: ReadTCState m => MetaId -> m Bool Source # | |||||
| UnFreezeMeta MetaId Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods 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 # | |||||
| ToJSON MetaId Source # | |||||
| NFData MetaId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum MetaId Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: MetaId -> MetaId Source # pred :: MetaId -> MetaId Source # toEnum :: Int -> MetaId Source # fromEnum :: MetaId -> Int Source # enumFrom :: MetaId -> [MetaId] Source # enumFromThen :: MetaId -> MetaId -> [MetaId] Source # enumFromTo :: MetaId -> MetaId -> [MetaId] Source # enumFromThenTo :: MetaId -> MetaId -> MetaId -> [MetaId] Source # | |||||
| Generic MetaId Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| 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 | |||||
| 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.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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.
Constructors
| Ranged | |
Fields
| |
Instances
| MapNamedArgPattern NAP Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
| Decoration Ranged Source # | |||||
| Functor Ranged Source # | |||||
| Foldable Ranged Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => Ranged m -> m Source # foldMap :: Monoid m => (a -> m) -> Ranged a -> m Source # foldMap' :: Monoid m => (a -> m) -> Ranged a -> m Source # foldr :: (a -> b -> b) -> b -> Ranged a -> b Source # foldr' :: (a -> b -> b) -> b -> Ranged a -> b Source # foldl :: (b -> a -> b) -> b -> Ranged a -> b Source # foldl' :: (b -> a -> b) -> b -> Ranged a -> b Source # foldr1 :: (a -> a -> a) -> Ranged a -> a Source # foldl1 :: (a -> a -> a) -> Ranged a -> a Source # toList :: Ranged a -> [a] Source # null :: Ranged a -> Bool Source # length :: Ranged a -> Int Source # elem :: Eq a => a -> Ranged a -> Bool Source # maximum :: Ord a => Ranged a -> a Source # minimum :: Ord a => Ranged a -> a Source # | |||||
| Traversable Ranged Source # | |||||
Defined in Agda.Syntax.Common | |||||
| MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
| ExprLike a => ExprLike (Ranged a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods 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 # | |||||
| PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
| HasRange (Ranged a) Source # | |||||
| KillRange (Ranged a) Source # | |||||
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Ranged a) Source # | |||||
| ToConcrete a => ToConcrete (Ranged a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
| |||||
| ToAbstract c => ToAbstract (Ranged c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types
| |||||
| Free t => Free (Ranged t) 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 Methods normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source # | |||||
| Normalise t => Normalise (Ranged t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
| EmbPrj a => EmbPrj (Ranged a) Source # | |||||
| Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
| Subst a => Subst (Ranged a) Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Ranged a)) -> Ranged a -> Ranged a Source # | |||||
| DeBruijn a => DeBruijn (Named_ a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn | |||||
| IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path Methods 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. | ||||
Defined in Agda.Syntax.Common | |||||
| 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 Methods 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 | |||||
| type SubstArg (Ranged a) Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
data ConstructorOrPatternSynonym Source #
Distinguish constructors from pattern synonyms.
Constructors
| IsConstructor | |
| IsPatternSynonym |
Instances
| Pretty ConstructorOrPatternSynonym Source # | |||||
Defined in Agda.Syntax.Common Methods pretty :: ConstructorOrPatternSynonym -> Doc Source # prettyPrec :: Int -> ConstructorOrPatternSynonym -> Doc Source # prettyList :: [ConstructorOrPatternSynonym] -> Doc Source # | |||||
| EmbPrj ConstructorOrPatternSynonym Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| NFData ConstructorOrPatternSynonym Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: ConstructorOrPatternSynonym -> () Source # | |||||
| Bounded ConstructorOrPatternSynonym Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum ConstructorOrPatternSynonym Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym Source # pred :: ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym Source # toEnum :: Int -> ConstructorOrPatternSynonym Source # fromEnum :: ConstructorOrPatternSynonym -> Int Source # enumFrom :: ConstructorOrPatternSynonym -> [ConstructorOrPatternSynonym] Source # enumFromThen :: ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym -> [ConstructorOrPatternSynonym] Source # enumFromTo :: ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym -> [ConstructorOrPatternSynonym] Source # enumFromThenTo :: ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym -> [ConstructorOrPatternSynonym] Source # | |||||
| Generic ConstructorOrPatternSynonym Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show ConstructorOrPatternSynonym Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type Rep ConstructorOrPatternSynonym Source # | |||||
Defined in Agda.Syntax.Common | |||||
A function argument can be hidden and/or irrelevant.
Constructors
| ArgInfo | |
Fields
| |
Instances
| LensAnnotation ArgInfo Source # | |
Defined in Agda.Syntax.Common Methods 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 Methods getFreeVariables :: ArgInfo -> FreeVariables Source # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo Source # | |
| LensHiding ArgInfo Source # | |
| LensLock ArgInfo Source # | |
| LensModalPolarity ArgInfo Source # | |
Defined in Agda.Syntax.Common Methods getModalPolarity :: ArgInfo -> PolarityModality Source # setModalPolarity :: PolarityModality -> ArgInfo -> ArgInfo Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> ArgInfo -> 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 Methods | |
| EqualSy ArgInfo Source # | Ignore origin and free variables. |
| ToTerm ArgInfo Source # | |
| ChooseFlex ArgInfo Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: ArgInfo -> ArgInfo -> FlexChoice Source # | |
| EmbPrj ArgInfo Source # | |
| SynEq ArgInfo Source # | |
| Unquote ArgInfo Source # | |
| Null ArgInfo Source # | |
| NFData ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
| Show ArgInfo Source # | |
| Eq ArgInfo Source # | |
| Ord ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
Where does the ConP or Con come from?
Constructors
| ConOSystem | Inserted by system or expanded from an implicit pattern. |
| ConOCon | User wrote a constructor (pattern). |
| ConORec | User wrote a record (pattern). |
| ConOSplit | Generated by interactive case splitting. |
Instances
| KillRange ConOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| EmbPrj ConOrigin Source # | |||||
| NFData ConOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Bounded ConOrigin Source # | |||||
| Enum ConOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: ConOrigin -> ConOrigin Source # pred :: ConOrigin -> ConOrigin Source # toEnum :: Int -> ConOrigin Source # fromEnum :: ConOrigin -> Int Source # enumFrom :: ConOrigin -> [ConOrigin] Source # enumFromThen :: ConOrigin -> ConOrigin -> [ConOrigin] Source # enumFromTo :: ConOrigin -> ConOrigin -> [ConOrigin] Source # enumFromThenTo :: ConOrigin -> ConOrigin -> ConOrigin -> [ConOrigin] Source # | |||||
| Generic ConOrigin Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| 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.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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))) | |||||
Constructors
| Hidden | |
| Instance Overlappable | |
| NotHidden |
Instances
| LensHiding Hiding Source # | |
| Pretty Hiding Source # | |
| HasRange Hiding Source # | |
| KillRange Hiding Source # | |
Defined in Agda.Syntax.Common Methods | |
| Verbalize Hiding Source # | |
| ChooseFlex Hiding Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods 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.
Minimal complete definition
Nothing
Methods
getOrigin :: a -> Origin Source #
default getOrigin :: LensArgInfo a => a -> Origin Source #
Instances
| LensOrigin ArgInfo Source # | |
| LensOrigin Origin Source # | |
| LensOrigin AppInfo Source # | |
| LensOrigin ContextEntry Source # | |
Defined in Agda.TypeChecking.Monad.Base.Types Methods getOrigin :: ContextEntry -> Origin Source # setOrigin :: Origin -> ContextEntry -> ContextEntry Source # mapOrigin :: (Origin -> Origin) -> ContextEntry -> ContextEntry Source # | |
| LensOrigin (Arg e) Source # | |
| LensOrigin (WithOrigin a) Source # | |
Defined in Agda.Syntax.Common Methods 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 Methods 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.
Constructors
| NameId !Word64 !ModuleNameHash |
Instances
| Pretty NameId Source # | |||||
| KillRange NameId Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| HasFresh NameId Source # | |||||
| EmbPrj NameId Source # | |||||
| NFData NameId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum NameId Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: NameId -> NameId Source # pred :: NameId -> NameId Source # toEnum :: Int -> NameId Source # fromEnum :: NameId -> Int Source # enumFrom :: NameId -> [NameId] Source # enumFromThen :: NameId -> NameId -> [NameId] Source # enumFromTo :: NameId -> NameId -> [NameId] Source # enumFromThenTo :: NameId -> NameId -> NameId -> [NameId] Source # | |||||
| Generic NameId Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show NameId Source # | |||||
| Eq NameId Source # | |||||
| Ord NameId Source # | |||||
| Hashable NameId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Monad m => MonadFresh NameId (PureConversionT m) Source # | |||||
Defined in Agda.TypeChecking.Conversion.Pure Methods 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.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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.
Constructors
| Named | |
Fields
| |
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 # | |||||
| Pretty e => Pretty (Named_ e) Source # | |||||
| PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
| 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 Methods 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 | |||||
| IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source # | |||||
| Decoration (Named name) Source # | |||||
| Functor (Named name) Source # | |||||
| Foldable (Named name) Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => Named name m -> m Source # foldMap :: Monoid m => (a -> m) -> Named name a -> m Source # foldMap' :: Monoid m => (a -> m) -> Named name a -> m Source # foldr :: (a -> b -> b) -> b -> Named name a -> b Source # foldr' :: (a -> b -> b) -> b -> Named name a -> b Source # foldl :: (b -> a -> b) -> b -> Named name a -> b Source # foldl' :: (b -> a -> b) -> b -> Named name a -> b Source # foldr1 :: (a -> a -> a) -> Named name a -> a Source # foldl1 :: (a -> a -> a) -> Named name a -> a Source # toList :: Named name a -> [a] Source # null :: Named name a -> Bool Source # length :: Named name a -> Int Source # elem :: Eq a => a -> Named name a -> Bool Source # maximum :: Ord a => Named name a -> a Source # minimum :: Ord a => Named name a -> a Source # | |||||
| Traversable (Named name) Source # | |||||
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> Named name a -> f (Named name b) Source # sequenceA :: Applicative f => Named name (f a) -> f (Named name a) Source # mapM :: Monad m => (a -> m b) -> Named name a -> m (Named name b) Source # sequence :: Monad m => Named name (m a) -> m (Named name a) 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 Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |||||
| APatternLike a => APatternLike (Named n a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern Associated Types
Methods 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 Methods declaredNames :: Collection KName m => Named name a -> m Source # | |||||
| ExprLike a => ExprLike (Named x a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods 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 Methods 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 Methods countPatternVars :: Named x a -> Int Source # | |||||
| PatternVarModalities a => PatternVarModalities (Named s a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern Associated Types
| |||||
| HasRange a => HasRange (Named name a) Source # | |||||
| (KillRange name, KillRange a) => KillRange (Named name a) Source # | |||||
Defined in Agda.Syntax.Common Methods 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 Associated Types
| |||||
| ToAbstract c => ToAbstract (Named name c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types
| |||||
| Reify i => Reify (Named n i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
| ToAbstract r => ToAbstract (Named name r) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types
Methods 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 Methods 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 Methods 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 Associated Types
Methods 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 Methods 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 Methods compare :: Named name a -> Named name a -> Ordering Source # (<) :: Named name a -> Named name a -> Bool Source # (<=) :: Named name a -> Named name a -> Bool Source # (>) :: Named name a -> Named name a -> Bool Source # (>=) :: Named name a -> Named name a -> Bool Source # max :: Named name a -> Named name a -> Named name a Source # min :: Named name a -> Named name a -> Named name a Source # | |||||
| 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 Associated Types
Methods 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.
Minimal complete definition
Nothing
Methods
getHiding :: a -> Hiding Source #
default getHiding :: LensArgInfo a => a -> Hiding Source #
Instances
| LensHiding LamBinding Source # | |
Defined in Agda.Syntax.Abstract Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |
| LensHiding TypedBinding Source # | |
Defined in Agda.Syntax.Abstract Methods 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 Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |
| LensHiding TypedBinding Source # | |
Defined in Agda.Syntax.Concrete Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source # | |
| LensHiding ContextEntry Source # | |
Defined in Agda.TypeChecking.Monad.Base.Types Methods getHiding :: ContextEntry -> Hiding Source # setHiding :: Hiding -> ContextEntry -> ContextEntry Source # mapHiding :: (Hiding -> Hiding) -> ContextEntry -> ContextEntry Source # | |
| LensHiding (Arg e) Source # | |
| LensHiding (WithHiding a) Source # | |
Defined in Agda.Syntax.Common Methods 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 Methods 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?
Constructors
| 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 Methods | |||||
| EmbPrj ProjOrigin Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| NFData ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: ProjOrigin -> () Source # | |||||
| Bounded ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: ProjOrigin -> ProjOrigin Source # pred :: ProjOrigin -> ProjOrigin Source # toEnum :: Int -> ProjOrigin Source # fromEnum :: ProjOrigin -> Int Source # enumFrom :: ProjOrigin -> [ProjOrigin] Source # enumFromThen :: ProjOrigin -> ProjOrigin -> [ProjOrigin] Source # enumFromTo :: ProjOrigin -> ProjOrigin -> [ProjOrigin] Source # enumFromThenTo :: ProjOrigin -> ProjOrigin -> ProjOrigin -> [ProjOrigin] Source # | |||||
| Generic ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: ProjOrigin -> ProjOrigin -> Bool Source # (/=) :: ProjOrigin -> ProjOrigin -> Bool Source # | |||||
| Ord ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: ProjOrigin -> ProjOrigin -> Ordering Source # (<) :: ProjOrigin -> ProjOrigin -> Bool Source # (<=) :: ProjOrigin -> ProjOrigin -> Bool Source # (>) :: ProjOrigin -> ProjOrigin -> Bool Source # (>=) :: ProjOrigin -> ProjOrigin -> Bool Source # max :: ProjOrigin -> ProjOrigin -> ProjOrigin Source # min :: ProjOrigin -> ProjOrigin -> ProjOrigin Source # | |||||
| type Rep ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common type Rep ProjOrigin = D1 ('MetaData "ProjOrigin" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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.
Constructors
| WithOrigin | |
Instances
| MapNamedArgPattern NAP Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
| Decoration WithOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods 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 Methods fmap :: (a -> b) -> WithOrigin a -> WithOrigin b Source # (<$) :: a -> WithOrigin b -> WithOrigin a Source # | |||||
| Foldable WithOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => WithOrigin m -> m Source # foldMap :: Monoid m => (a -> m) -> WithOrigin a -> m Source # foldMap' :: Monoid m => (a -> m) -> WithOrigin a -> m Source # foldr :: (a -> b -> b) -> b -> WithOrigin a -> b Source # foldr' :: (a -> b -> b) -> b -> WithOrigin a -> b Source # foldl :: (b -> a -> b) -> b -> WithOrigin a -> b Source # foldl' :: (b -> a -> b) -> b -> WithOrigin a -> b Source # foldr1 :: (a -> a -> a) -> WithOrigin a -> a Source # foldl1 :: (a -> a -> a) -> WithOrigin a -> a Source # toList :: WithOrigin a -> [a] Source # null :: WithOrigin a -> Bool Source # length :: WithOrigin a -> Int Source # elem :: Eq a => a -> WithOrigin a -> Bool Source # maximum :: Ord a => WithOrigin a -> a Source # minimum :: Ord a => WithOrigin a -> a Source # sum :: Num a => WithOrigin a -> a Source # product :: Num a => WithOrigin a -> a Source # | |||||
| Traversable WithOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> WithOrigin a -> f (WithOrigin b) Source # sequenceA :: Applicative f => WithOrigin (f a) -> f (WithOrigin a) Source # mapM :: Monad m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) Source # sequence :: Monad m => WithOrigin (m a) -> m (WithOrigin a) Source # | |||||
| MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
| LensOrigin (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common Methods 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 Methods 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 Methods isNoName :: WithOrigin a -> Bool Source # | |||||
| PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
| HasRange a => HasRange (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common Methods getRange :: WithOrigin a -> Range Source # | |||||
| KillRange a => KillRange (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (WithOrigin a) Source # | |||||
| SetRange a => SetRange (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common Methods 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 Methods normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source # | |||||
| EmbPrj a => EmbPrj (WithOrigin a) Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
| DeBruijn a => DeBruijn (Named_ a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn | |||||
| IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source # | |||||
| NFData a => NFData (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: WithOrigin a -> () Source # | |||||
| Show a => Show (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq a => Eq (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: WithOrigin a -> WithOrigin a -> Bool Source # (/=) :: WithOrigin a -> WithOrigin a -> Bool Source # | |||||
| Ord a => Ord (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: WithOrigin a -> WithOrigin a -> Ordering Source # (<) :: WithOrigin a -> WithOrigin a -> Bool Source # (<=) :: WithOrigin a -> WithOrigin a -> Bool Source # (>) :: WithOrigin a -> WithOrigin a -> Bool Source # (>=) :: WithOrigin a -> WithOrigin a -> Bool Source # max :: WithOrigin a -> WithOrigin a -> WithOrigin a Source # min :: WithOrigin a -> WithOrigin a -> WithOrigin a Source # | |||||
| 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 Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
| type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
data TerminationCheck m Source #
Termination check? (Default = TerminationCheck).
Constructors
| TerminationCheck | Run the termination checker. |
| NoTerminationCheck | Skip termination checking (unsafe). |
| NonTerminating | Treat as non-terminating. |
| Terminating | Treat as terminating (unsafe). Same effect as |
| TerminationMeasure Range m | Skip termination checking but use measure instead. |
Instances
| Functor TerminationCheck Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> TerminationCheck a -> TerminationCheck b Source # (<$) :: a -> TerminationCheck b -> TerminationCheck a Source # | |
| KillRange m => KillRange (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (TerminationCheck m) Source # | |
| NFData a => NFData (TerminationCheck a) Source # | |
Defined in Agda.Syntax.Common Methods rnf :: TerminationCheck a -> () Source # | |
| Show m => Show (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common | |
| Eq m => Eq (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: TerminationCheck m -> TerminationCheck m -> Bool Source # (/=) :: TerminationCheck m -> TerminationCheck m -> Bool Source # | |
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.
Constructors
| Flat | same points, discrete topology, idempotent comonad, box-like. |
| Continuous | identity modality. | Sharp -- ^ same points, codiscrete topology, idempotent monad, diamond-like. |
| Squash | single point space, artificially added for Flat left-composition. |
Instances
| LensCohesion Cohesion Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Pretty Cohesion Source # | |||||
| HasRange Cohesion Source # | |||||
| KillRange Cohesion Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| SetRange Cohesion Source # | |||||
| Verbalize Cohesion Source # | |||||
| EmbPrj Cohesion Source # | |||||
| Null Cohesion Source # |
| ||||
| PartialOrd Cohesion Source # | Flatter is smaller. | ||||
Defined in Agda.Syntax.Common Methods | |||||
| NFData Cohesion Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Bounded Cohesion Source # | |||||
| Enum Cohesion Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: Cohesion -> Cohesion Source # pred :: Cohesion -> Cohesion Source # toEnum :: Int -> Cohesion Source # fromEnum :: Cohesion -> Int Source # enumFrom :: Cohesion -> [Cohesion] Source # enumFromThen :: Cohesion -> Cohesion -> [Cohesion] Source # enumFromTo :: Cohesion -> Cohesion -> [Cohesion] Source # enumFromThenTo :: Cohesion -> Cohesion -> Cohesion -> [Cohesion] Source # | |||||
| Generic Cohesion Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Cohesion Source # | |||||
| Eq Cohesion Source # | |||||
| Ord Cohesion Source # | Order is given by implication: flatter is smaller. | ||||
Defined in Agda.Syntax.Common | |||||
| LeftClosedPOMonoid (UnderComposition Cohesion) Source # | |||||
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion Source # | |||||
| 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 Methods mempty :: UnderAddition Cohesion Source # mappend :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion Source # mconcat :: [UnderAddition Cohesion] -> UnderAddition Cohesion Source # | |||||
| Monoid (UnderComposition Cohesion) Source # |
| ||||
Defined in Agda.Syntax.Common | |||||
| Semigroup (UnderAddition Cohesion) Source # |
| ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion Source # sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion Source # stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion Source # | |||||
| Semigroup (UnderComposition Cohesion) Source # |
| ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion Source # sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion Source # stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion Source # | |||||
| type Rep Cohesion Source # | |||||
Defined in Agda.Syntax.Common type Rep Cohesion = D1 ('MetaData "Cohesion" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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 #
Constructors
| RecordDirectives | |
Fields
| |
Instances
| DeclaredNames RecordDirectives Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RecordDirectives -> m Source # | |||||
| ToConcrete RecordDirectives Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => RecordDirectives -> m (ConOfAbs RecordDirectives) Source # bindToConcrete :: MonadToConcrete m => RecordDirectives -> (ConOfAbs RecordDirectives -> m b) -> m b Source # | |||||
| Functor RecordDirectives' Source # | |||||
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> RecordDirectives' a -> RecordDirectives' b Source # (<$) :: a -> RecordDirectives' b -> RecordDirectives' a Source # | |||||
| Foldable RecordDirectives' Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => RecordDirectives' m -> m Source # foldMap :: Monoid m => (a -> m) -> RecordDirectives' a -> m Source # foldMap' :: Monoid m => (a -> m) -> RecordDirectives' a -> m Source # foldr :: (a -> b -> b) -> b -> RecordDirectives' a -> b Source # foldr' :: (a -> b -> b) -> b -> RecordDirectives' a -> b Source # foldl :: (b -> a -> b) -> b -> RecordDirectives' a -> b Source # foldl' :: (b -> a -> b) -> b -> RecordDirectives' a -> b Source # foldr1 :: (a -> a -> a) -> RecordDirectives' a -> a Source # foldl1 :: (a -> a -> a) -> RecordDirectives' a -> a Source # toList :: RecordDirectives' a -> [a] Source # null :: RecordDirectives' a -> Bool Source # length :: RecordDirectives' a -> Int Source # elem :: Eq a => a -> RecordDirectives' a -> Bool Source # maximum :: Ord a => RecordDirectives' a -> a Source # minimum :: Ord a => RecordDirectives' a -> a Source # sum :: Num a => RecordDirectives' a -> a Source # product :: Num a => RecordDirectives' a -> a Source # | |||||
| Traversable RecordDirectives' Source # | |||||
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> RecordDirectives' a -> f (RecordDirectives' b) Source # sequenceA :: Applicative f => RecordDirectives' (f a) -> f (RecordDirectives' a) Source # mapM :: Monad m => (a -> m b) -> RecordDirectives' a -> m (RecordDirectives' b) Source # sequence :: Monad m => RecordDirectives' (m a) -> m (RecordDirectives' a) Source # | |||||
| HasRange a => HasRange (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common Methods getRange :: RecordDirectives' a -> Range Source # | |||||
| KillRange a => KillRange (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (RecordDirectives' a) Source # | |||||
| EmbPrj a => EmbPrj (RecordDirectives' a) Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| Null a => Null (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| NFData a => NFData (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: RecordDirectives' a -> () Source # | |||||
| Show a => Show (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq a => Eq (RecordDirectives' a) Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: RecordDirectives' a -> RecordDirectives' a -> Bool Source # (/=) :: RecordDirectives' a -> RecordDirectives' a -> Bool Source # | |||||
| type ConOfAbs RecordDirectives Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
The using clause of import directive.
Constructors
| 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 Methods 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 m, Show n) => Show (Using' n m) Source # | |
| (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.
Constructors
| ImportedModule m | Imported module name of type |
| ImportedName n | Imported name of type |
Instances
| PrettyTCM ImportedName Source # | |
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ImportedName -> m Doc Source # | |
| (Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common Methods 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 Methods getRange :: ImportedName' a b -> Range Source # | |
| (KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportedName' a b) Source # | |
| (EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| (NFData a, NFData b) => NFData (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common Methods rnf :: ImportedName' a b -> () Source # | |
| (Show m, Show n) => Show (ImportedName' n m) Source # | |
Defined in Agda.Syntax.Common | |
| (Eq m, Eq n) => Eq (ImportedName' n m) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: ImportedName' n m -> ImportedName' n m -> Bool Source # (/=) :: ImportedName' n m -> ImportedName' n m -> Bool Source # | |
| (Ord m, Ord n) => Ord (ImportedName' n m) Source # | |
Defined in Agda.Syntax.Common Methods compare :: ImportedName' n m -> ImportedName' n m -> Ordering Source # (<) :: ImportedName' n m -> ImportedName' n m -> Bool Source # (<=) :: ImportedName' n m -> ImportedName' n m -> Bool Source # (>) :: ImportedName' n m -> ImportedName' n m -> Bool Source # (>=) :: ImportedName' n m -> ImportedName' n m -> Bool Source # max :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m Source # min :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m Source # | |
Constructors
| Renaming | |
Fields
| |
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 Methods 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 m, Show n) => Show (Renaming' n m) Source # | |
| (Eq m, Eq n) => Eq (Renaming' n m) Source # | |
Variants of Cubical Agda.
Agda variants.
Only some variants are tracked.
Instances
| KillRange Language Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| EmbPrj Language Source # | |||||
| NFData Language Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic Language Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| 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.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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)))) | |||||
class LensArgInfo a where Source #
Minimal complete definition
Methods
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 Methods getArgInfo :: Definition -> ArgInfo Source # setArgInfo :: ArgInfo -> Definition -> Definition Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Definition -> Definition Source # | |
| LensArgInfo ContextEntry Source # | |
Defined in Agda.TypeChecking.Monad.Base.Types Methods getArgInfo :: ContextEntry -> ArgInfo Source # setArgInfo :: ArgInfo -> ContextEntry -> ContextEntry Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> ContextEntry -> ContextEntry Source # | |
| LensArgInfo (Arg a) Source # | |
Defined in Agda.Syntax.Common | |
| LensArgInfo (FlexibleVar a) Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods 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 | |
class LensCohesion a where Source #
A lens to access the Cohesion attribute in data structures.
Minimal implementation: getCohesion and mapCohesion or LensModality.
Minimal complete definition
Nothing
Methods
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 ContextEntry Source # | |
Defined in Agda.TypeChecking.Monad.Base.Types Methods getCohesion :: ContextEntry -> Cohesion Source # setCohesion :: Cohesion -> ContextEntry -> ContextEntry Source # mapCohesion :: (Cohesion -> Cohesion) -> ContextEntry -> ContextEntry Source # | |
| LensCohesion (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
| LensCohesion (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal | |
class LensModality a where Source #
Minimal complete definition
Nothing
Methods
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 Methods 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 Methods getModality :: MetaVariable -> Modality Source # setModality :: Modality -> MetaVariable -> MetaVariable Source # mapModality :: (Modality -> Modality) -> MetaVariable -> MetaVariable Source # | |
| LensModality RemoteMetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getModality :: RemoteMetaVariable -> Modality Source # setModality :: Modality -> RemoteMetaVariable -> RemoteMetaVariable Source # mapModality :: (Modality -> Modality) -> RemoteMetaVariable -> RemoteMetaVariable Source # | |
| LensModality ContextEntry Source # | |
Defined in Agda.TypeChecking.Monad.Base.Types Methods getModality :: ContextEntry -> Modality Source # setModality :: Modality -> ContextEntry -> ContextEntry Source # mapModality :: (Modality -> Modality) -> ContextEntry -> ContextEntry 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 Methods 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 | |
class LensQuantity a where Source #
Minimal complete definition
Nothing
Methods
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 Methods 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 Methods getQuantity :: MetaVariable -> Quantity Source # setQuantity :: Quantity -> MetaVariable -> MetaVariable Source # mapQuantity :: (Quantity -> Quantity) -> MetaVariable -> MetaVariable Source # | |
| LensQuantity RemoteMetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getQuantity :: RemoteMetaVariable -> Quantity Source # setQuantity :: Quantity -> RemoteMetaVariable -> RemoteMetaVariable Source # mapQuantity :: (Quantity -> Quantity) -> RemoteMetaVariable -> RemoteMetaVariable Source # | |
| LensQuantity ContextEntry Source # | |
Defined in Agda.TypeChecking.Monad.Base.Types Methods getQuantity :: ContextEntry -> Quantity Source # setQuantity :: Quantity -> ContextEntry -> ContextEntry Source # mapQuantity :: (Quantity -> Quantity) -> ContextEntry -> ContextEntry 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 | |
class LensRelevance a where Source #
A lens to access the Relevance attribute in data structures.
Minimal implementation: getRelevance and mapRelevance or LensModality.
Minimal complete definition
Nothing
Methods
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 Methods getRelevance :: TypedBinding -> Relevance Source # setRelevance :: Relevance -> TypedBinding -> TypedBinding Source # mapRelevance :: (Relevance -> Relevance) -> TypedBinding -> TypedBinding Source # | |
| LensRelevance Definition Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods 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 Methods getRelevance :: MetaVariable -> Relevance Source # setRelevance :: Relevance -> MetaVariable -> MetaVariable Source # mapRelevance :: (Relevance -> Relevance) -> MetaVariable -> MetaVariable Source # | |
| LensRelevance RemoteMetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getRelevance :: RemoteMetaVariable -> Relevance Source # setRelevance :: Relevance -> RemoteMetaVariable -> RemoteMetaVariable Source # mapRelevance :: (Relevance -> Relevance) -> RemoteMetaVariable -> RemoteMetaVariable Source # | |
| LensRelevance ContextEntry Source # | |
Defined in Agda.TypeChecking.Monad.Base.Types Methods getRelevance :: ContextEntry -> Relevance Source # setRelevance :: Relevance -> ContextEntry -> ContextEntry Source # mapRelevance :: (Relevance -> Relevance) -> ContextEntry -> ContextEntry Source # | |
| 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 | |
class LensModalPolarity a where Source #
A lens to access the PolarityModality attribute in data structures.
Minimal implementation: getModalPolarity and mapModalPolarity or LensModality.
Minimal complete definition
Nothing
Methods
getModalPolarity :: a -> PolarityModality Source #
default getModalPolarity :: LensModality a => a -> PolarityModality Source #
setModalPolarity :: PolarityModality -> a -> a Source #
mapModalPolarity :: (PolarityModality -> PolarityModality) -> a -> a Source #
default mapModalPolarity :: LensModality a => (PolarityModality -> PolarityModality) -> a -> a Source #
Instances
| LensModalPolarity ArgInfo Source # | |
Defined in Agda.Syntax.Common Methods getModalPolarity :: ArgInfo -> PolarityModality Source # setModalPolarity :: PolarityModality -> ArgInfo -> ArgInfo Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> ArgInfo -> ArgInfo Source # | |
| LensModalPolarity Modality Source # | |
Defined in Agda.Syntax.Common Methods getModalPolarity :: Modality -> PolarityModality Source # setModalPolarity :: PolarityModality -> Modality -> Modality Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> Modality -> Modality Source # | |
| LensModalPolarity PolarityModality Source # | |
Defined in Agda.Syntax.Common | |
| LensModalPolarity Definition Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getModalPolarity :: Definition -> PolarityModality Source # setModalPolarity :: PolarityModality -> Definition -> Definition Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> Definition -> Definition Source # | |
| LensModalPolarity MetaInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getModalPolarity :: MetaInfo -> PolarityModality Source # setModalPolarity :: PolarityModality -> MetaInfo -> MetaInfo Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> MetaInfo -> MetaInfo Source # | |
| LensModalPolarity RemoteMetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| LensModalPolarity ContextEntry Source # | |
Defined in Agda.TypeChecking.Monad.Base.Types Methods getModalPolarity :: ContextEntry -> PolarityModality Source # setModalPolarity :: PolarityModality -> ContextEntry -> ContextEntry Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> ContextEntry -> ContextEntry Source # | |
| LensModalPolarity (Arg e) Source # | |
Defined in Agda.Syntax.Common Methods getModalPolarity :: Arg e -> PolarityModality Source # setModalPolarity :: PolarityModality -> Arg e -> Arg e Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> Arg e -> Arg e Source # | |
| LensModalPolarity (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal Methods getModalPolarity :: Dom' t e -> PolarityModality Source # setModalPolarity :: PolarityModality -> Dom' t e -> Dom' t e Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> Dom' t e -> Dom' t e Source # | |
fromImportedName :: ImportedName' a a -> a Source #
partitionImportedNames :: [ImportedName' n m] -> ([n], [m]) Source #
Like partitionEithers.
Opaque or transparent.
Constructors
| 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 Methods jointOpacity :: IsOpaque -> JointOpacity Source # | |||||
| LensIsOpaque IsOpaque Source # | |||||
Defined in Agda.Syntax.Common | |||||
| KillRange IsOpaque Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| EmbPrj IsOpaque Source # | |||||
| NFData IsOpaque Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic IsOpaque Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show IsOpaque Source # | |||||
| Eq IsOpaque Source # | |||||
| Ord IsOpaque Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type Rep IsOpaque Source # | |||||
Defined in Agda.Syntax.Common type Rep IsOpaque = D1 ('MetaData "IsOpaque" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) (C1 ('MetaCons "OpaqueDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 OpaqueId)) :+: C1 ('MetaCons "TransparentDef" 'PrefixI 'False) (U1 :: Type -> Type)) | |||||
hasQuantity0 :: LensQuantity a => a -> Bool Source #
Check for Quantity0.
data WithHiding a Source #
Decorating something with Hiding information.
Constructors
| WithHiding | |
Instances
| Decoration WithHiding Source # | |||||
Defined in Agda.Syntax.Common Methods 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 Methods pure :: a -> WithHiding a Source # (<*>) :: WithHiding (a -> b) -> WithHiding a -> WithHiding b Source # liftA2 :: (a -> b -> c) -> WithHiding a -> WithHiding b -> WithHiding c Source # (*>) :: WithHiding a -> WithHiding b -> WithHiding b Source # (<*) :: WithHiding a -> WithHiding b -> WithHiding a Source # | |||||
| Functor WithHiding Source # | |||||
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> WithHiding a -> WithHiding b Source # (<$) :: a -> WithHiding b -> WithHiding a Source # | |||||
| Foldable WithHiding Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => WithHiding m -> m Source # foldMap :: Monoid m => (a -> m) -> WithHiding a -> m Source # foldMap' :: Monoid m => (a -> m) -> WithHiding a -> m Source # foldr :: (a -> b -> b) -> b -> WithHiding a -> b Source # foldr' :: (a -> b -> b) -> b -> WithHiding a -> b Source # foldl :: (b -> a -> b) -> b -> WithHiding a -> b Source # foldl' :: (b -> a -> b) -> b -> WithHiding a -> b Source # foldr1 :: (a -> a -> a) -> WithHiding a -> a Source # foldl1 :: (a -> a -> a) -> WithHiding a -> a Source # toList :: WithHiding a -> [a] Source # null :: WithHiding a -> Bool Source # length :: WithHiding a -> Int Source # elem :: Eq a => a -> WithHiding a -> Bool Source # maximum :: Ord a => WithHiding a -> a Source # minimum :: Ord a => WithHiding a -> a Source # sum :: Num a => WithHiding a -> a Source # product :: Num a => WithHiding a -> a Source # | |||||
| Traversable WithHiding Source # | |||||
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> WithHiding a -> f (WithHiding b) Source # sequenceA :: Applicative f => WithHiding (f a) -> f (WithHiding a) Source # mapM :: Monad m => (a -> m b) -> WithHiding a -> m (WithHiding b) Source # sequence :: Monad m => WithHiding (m a) -> m (WithHiding a) Source # | |||||
| ExprLike a => ExprLike (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods 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 Methods 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.Common Methods 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 Methods 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 Methods 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 Methods getRange :: WithHiding a -> Range Source # | |||||
| KillRange a => KillRange (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (WithHiding a) Source # | |||||
| SetRange a => SetRange (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common Methods setRange :: Range -> WithHiding a -> WithHiding a Source # | |||||
| ToConcrete a => ToConcrete (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => WithHiding a -> m (ConOfAbs (WithHiding a)) Source # bindToConcrete :: MonadToConcrete m => WithHiding a -> (ConOfAbs (WithHiding a) -> m b) -> m b Source # | |||||
| ToAbstract c => ToAbstract (WithHiding c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types
Methods 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 Methods prettyTCM :: MonadPretty m => WithHiding a -> m Doc Source # | |||||
| Normalise t => Normalise (WithHiding t) Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods normalise' :: WithHiding t -> ReduceM (WithHiding t) Source # | |||||
| EmbPrj a => EmbPrj (WithHiding a) Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| Subst a => Subst (WithHiding a) Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (WithHiding a)) -> WithHiding a -> WithHiding a Source # | |||||
| NFData a => NFData (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: WithHiding a -> () Source # | |||||
| Show a => Show (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq a => Eq (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: WithHiding a -> WithHiding a -> Bool Source # (/=) :: WithHiding a -> WithHiding a -> Bool Source # | |||||
| Ord a => Ord (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: WithHiding a -> WithHiding a -> Ordering Source # (<) :: WithHiding a -> WithHiding a -> Bool Source # (<=) :: WithHiding a -> WithHiding a -> Bool Source # (>) :: WithHiding a -> WithHiding a -> Bool Source # (>=) :: WithHiding a -> WithHiding a -> Bool Source # max :: WithHiding a -> WithHiding a -> WithHiding a Source # min :: WithHiding a -> WithHiding a -> WithHiding a Source # | |||||
| AddContext (List1 (WithHiding Name), Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods 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 Methods 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 | |||||
data PolarityModality Source #
Constructors
| PolarityModality | |
Fields
| |
Instances
| LensModalPolarity PolarityModality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Pretty PolarityModality Source # | |||||
Defined in Agda.Syntax.Common Methods pretty :: PolarityModality -> Doc Source # prettyPrec :: Int -> PolarityModality -> Doc Source # prettyList :: [PolarityModality] -> Doc Source # | |||||
| HasRange PolarityModality Source # | |||||
Defined in Agda.Syntax.Common Methods getRange :: PolarityModality -> Range Source # | |||||
| KillRange PolarityModality Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| SetRange PolarityModality Source # | |||||
Defined in Agda.Syntax.Common Methods setRange :: Range -> PolarityModality -> PolarityModality Source # | |||||
| Verbalize PolarityModality Source # | |||||
Defined in Agda.TypeChecking.Errors Methods verbalize :: PolarityModality -> String Source # | |||||
| PrettyTCM PolarityModality Source # | |||||
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => PolarityModality -> m Doc Source # | |||||
| EmbPrj PolarityModality Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| Null PolarityModality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| PartialOrd PolarityModality Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| NFData PolarityModality Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: PolarityModality -> () Source # | |||||
| Bounded PolarityModality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic PolarityModality Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods from :: PolarityModality -> Rep PolarityModality x Source # to :: Rep PolarityModality x -> PolarityModality Source # | |||||
| Show PolarityModality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq PolarityModality Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: PolarityModality -> PolarityModality -> Bool Source # (/=) :: PolarityModality -> PolarityModality -> Bool Source # | |||||
| Ord PolarityModality Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: PolarityModality -> PolarityModality -> Ordering Source # (<) :: PolarityModality -> PolarityModality -> Bool Source # (<=) :: PolarityModality -> PolarityModality -> Bool Source # (>) :: PolarityModality -> PolarityModality -> Bool Source # (>=) :: PolarityModality -> PolarityModality -> Bool Source # max :: PolarityModality -> PolarityModality -> PolarityModality Source # min :: PolarityModality -> PolarityModality -> PolarityModality Source # | |||||
| LeftClosedPOMonoid (UnderComposition PolarityModality) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| POMonoid (UnderAddition PolarityModality) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| POMonoid (UnderComposition PolarityModality) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| POSemigroup (UnderAddition PolarityModality) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| POSemigroup (UnderComposition PolarityModality) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Monoid (UnderAddition PolarityModality) Source # | '' is the additive unit. | ||||
| Monoid (UnderComposition PolarityModality) Source # |
| ||||
Defined in Agda.Syntax.Common | |||||
| Semigroup (UnderAddition PolarityModality) Source # |
| ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition PolarityModality -> UnderAddition PolarityModality -> UnderAddition PolarityModality Source # sconcat :: NonEmpty (UnderAddition PolarityModality) -> UnderAddition PolarityModality Source # stimes :: Integral b => b -> UnderAddition PolarityModality -> UnderAddition PolarityModality Source # | |||||
| Semigroup (UnderComposition PolarityModality) Source # |
| ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition PolarityModality -> UnderComposition PolarityModality -> UnderComposition PolarityModality Source # sconcat :: NonEmpty (UnderComposition PolarityModality) -> UnderComposition PolarityModality Source # stimes :: Integral b => b -> UnderComposition PolarityModality -> UnderComposition PolarityModality Source # | |||||
| type Rep PolarityModality Source # | |||||
Defined in Agda.Syntax.Common type Rep PolarityModality = D1 ('MetaData "PolarityModality" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) (C1 ('MetaCons "PolarityModality" 'PrefixI 'True) (S1 ('MetaSel ('Just "modPolarityAnn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModalPolarity) :*: (S1 ('MetaSel ('Just "modPolarityOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModalPolarity) :*: S1 ('MetaSel ('Just "modPolarityLock") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModalPolarity)))) | |||||
A function argument can be relevant or irrelevant. See Agda.TypeChecking.Irrelevance.
Constructors
| Relevant OriginRelevant | The argument is (possibly) relevant at compile-time. |
| ShapeIrrelevant OriginShapeIrrelevant | Like Unlike |
| Irrelevant OriginIrrelevant | 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 Methods | |||||
| SetRange Relevance Source # | |||||
| Verbalize Relevance Source # | |||||
| PrettyTCM Relevance Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| EmbPrj Relevance Source # | |||||
| Unquote Relevance Source # | |||||
| Null Relevance Source # |
| ||||
| PartialOrd Relevance Source # | More relevant is smaller. | ||||
Defined in Agda.Syntax.Common Methods | |||||
| NFData Relevance Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic Relevance Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| 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 Methods inverseCompose :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance Source # | |||||
| 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 Methods mempty :: UnderAddition Relevance Source # mappend :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance Source # mconcat :: [UnderAddition Relevance] -> UnderAddition Relevance Source # | |||||
| Monoid (UnderComposition Relevance) Source # |
| ||||
Defined in Agda.Syntax.Common | |||||
| Semigroup (UnderAddition Relevance) Source # | |||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance Source # sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance Source # stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance Source # | |||||
| Semigroup (UnderComposition Relevance) Source # |
| ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance Source # sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance Source # stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance Source # | |||||
| type Rep Relevance Source # | |||||
Defined in Agda.Syntax.Common type Rep Relevance = D1 ('MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) (C1 ('MetaCons "Relevant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OriginRelevant)) :+: (C1 ('MetaCons "ShapeIrrelevant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OriginShapeIrrelevant)) :+: C1 ('MetaCons "Irrelevant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OriginIrrelevant)))) | |||||
cubicalOptionString :: Cubical -> String Source #
data DisplayLHS Source #
Distinguish parsing a DISPLAY pragma from an ordinary left hand side.
Constructors
| YesDisplayLHS | |
| NoDisplayLHS |
Instances
| Boolean DisplayLHS Source # | |||||
Defined in Agda.Syntax.Common Methods fromBool :: Bool -> DisplayLHS Source # true :: DisplayLHS Source # false :: DisplayLHS Source # not :: DisplayLHS -> DisplayLHS Source # (&&) :: DisplayLHS -> DisplayLHS -> DisplayLHS Source # (||) :: DisplayLHS -> DisplayLHS -> DisplayLHS Source # implies :: DisplayLHS -> DisplayLHS -> DisplayLHS Source # butNot :: DisplayLHS -> DisplayLHS -> DisplayLHS Source # | |||||
| IsBool DisplayLHS Source # | |||||
Defined in Agda.Syntax.Common Methods toBool :: DisplayLHS -> Bool Source # ifThenElse :: DisplayLHS -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> DisplayLHS -> DisplayLHS Source # fromBool2 :: (Bool -> Bool -> Bool) -> DisplayLHS -> DisplayLHS -> DisplayLHS Source # | |||||
| Bounded DisplayLHS Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum DisplayLHS Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: DisplayLHS -> DisplayLHS Source # pred :: DisplayLHS -> DisplayLHS Source # toEnum :: Int -> DisplayLHS Source # fromEnum :: DisplayLHS -> Int Source # enumFrom :: DisplayLHS -> [DisplayLHS] Source # enumFromThen :: DisplayLHS -> DisplayLHS -> [DisplayLHS] Source # enumFromTo :: DisplayLHS -> DisplayLHS -> [DisplayLHS] Source # enumFromThenTo :: DisplayLHS -> DisplayLHS -> DisplayLHS -> [DisplayLHS] Source # | |||||
| Generic DisplayLHS Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show DisplayLHS Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq DisplayLHS Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: DisplayLHS -> DisplayLHS -> Bool Source # (/=) :: DisplayLHS -> DisplayLHS -> Bool Source # | |||||
| type Rep DisplayLHS Source # | |||||
emptyRecordDirectives :: Null a => RecordDirectives' a Source #
Does a record come with eta-equality?
Instances
| CopatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods | |
| PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
| Functor HasEta' Source # | |
| Foldable HasEta' Source # | |
Defined in Agda.Syntax.Common Methods fold :: Monoid m => HasEta' m -> m Source # foldMap :: Monoid m => (a -> m) -> HasEta' a -> m Source # foldMap' :: Monoid m => (a -> m) -> HasEta' a -> m Source # foldr :: (a -> b -> b) -> b -> HasEta' a -> b Source # foldr' :: (a -> b -> b) -> b -> HasEta' a -> b Source # foldl :: (b -> a -> b) -> b -> HasEta' a -> b Source # foldl' :: (b -> a -> b) -> b -> HasEta' a -> b Source # foldr1 :: (a -> a -> a) -> HasEta' a -> a Source # foldl1 :: (a -> a -> a) -> HasEta' a -> a Source # toList :: HasEta' a -> [a] Source # null :: HasEta' a -> Bool Source # length :: HasEta' a -> Int Source # elem :: Eq a => a -> HasEta' a -> Bool Source # maximum :: Ord a => HasEta' a -> a Source # minimum :: Ord a => HasEta' a -> a Source # | |
| Traversable HasEta' Source # | |
Defined in Agda.Syntax.Common | |
| HasRange a => HasRange (HasEta' a) Source # | |
| KillRange a => KillRange (HasEta' a) Source # | |
Defined in Agda.Syntax.Common Methods 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?
Constructors
| PatternMatching | Can match on the record constructor. |
| CopatternMatching | Can copattern match using the projections. (Default.) |
Instances
| CopatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods | |
| CopatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
| CopatternMatchingAllowed DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods | |
| PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
| PatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
| PatternMatchingAllowed DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods | |
| HasRange PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods getRange :: PatternOrCopattern -> Range Source # | |
| KillRange PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods | |
| KillRange DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods | |
| EmbPrj PatternOrCopattern Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| EmbPrj DataOrRecord Source # | |
| NFData PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods rnf :: PatternOrCopattern -> () Source # | |
| Bounded PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common | |
| Enum PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods succ :: PatternOrCopattern -> PatternOrCopattern Source # pred :: PatternOrCopattern -> PatternOrCopattern Source # toEnum :: Int -> PatternOrCopattern Source # fromEnum :: PatternOrCopattern -> Int Source # enumFrom :: PatternOrCopattern -> [PatternOrCopattern] Source # enumFromThen :: PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] Source # enumFromTo :: PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] Source # enumFromThenTo :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] Source # | |
| Show PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common | |
| Eq PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods (==) :: PatternOrCopattern -> PatternOrCopattern -> Bool Source # (/=) :: PatternOrCopattern -> PatternOrCopattern -> Bool Source # | |
| Ord PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods compare :: PatternOrCopattern -> PatternOrCopattern -> Ordering Source # (<) :: PatternOrCopattern -> PatternOrCopattern -> Bool Source # (<=) :: PatternOrCopattern -> PatternOrCopattern -> Bool Source # (>) :: PatternOrCopattern -> PatternOrCopattern -> Bool Source # (>=) :: PatternOrCopattern -> PatternOrCopattern -> Bool Source # max :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern Source # min :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern Source # | |
class PatternMatchingAllowed a where Source #
Can we pattern match on the record constructor?
Methods
patternMatchingAllowed :: a -> Bool Source #
Instances
| PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
| PatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
| PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
| PatternMatchingAllowed DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods | |
| PatternMatchingAllowed EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
class CopatternMatchingAllowed a where Source #
Can we construct a record by copattern matching?
Methods
copatternMatchingAllowed :: a -> Bool Source #
Instances
| CopatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods | |
| CopatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
| CopatternMatchingAllowed ConHead Source # | |
Defined in Agda.Syntax.Internal Methods | |
| CopatternMatchingAllowed DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods | |
| CopatternMatchingAllowed EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
class HasOverlapMode a where Source #
Methods
Instances
| HasOverlapMode OverlapMode Source # | |
Defined in Agda.Syntax.Common Methods | |
| HasOverlapMode Candidate Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
isIncoherent :: HasOverlapMode a => a -> Bool Source #
isOverlappable :: HasOverlapMode a => a -> Bool Source #
isOverlapping :: HasOverlapMode a => a -> Bool Source #
hidingToString :: Hiding -> String Source #
mergeHiding :: LensHiding a => WithHiding a -> a Source #
Monoidal composition of Hiding information in some data.
notVisible :: LensHiding a => a -> Bool Source #
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.
prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc Source #
prettyHiding info visible doc puts the correct braces
around doc according to info info and returns
visible doc if the we deal with a visible thing.
newtype UnderAddition t Source #
Type wrapper to indicate additive monoid/semigroup context.
Constructors
| UnderAddition t |
Instances
| Applicative UnderAddition Source # | |
Defined in Agda.Syntax.Common Methods pure :: a -> UnderAddition a Source # (<*>) :: UnderAddition (a -> b) -> UnderAddition a -> UnderAddition b Source # liftA2 :: (a -> b -> c) -> UnderAddition a -> UnderAddition b -> UnderAddition c Source # (*>) :: UnderAddition a -> UnderAddition b -> UnderAddition b Source # (<*) :: UnderAddition a -> UnderAddition b -> UnderAddition a Source # | |
| Functor UnderAddition Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> UnderAddition a -> UnderAddition b Source # (<$) :: a -> UnderAddition b -> UnderAddition a Source # | |
| POMonoid (UnderAddition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
| POMonoid (UnderAddition Modality) Source # | |
Defined in Agda.Syntax.Common | |
| POMonoid (UnderAddition PolarityModality) 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 PolarityModality) 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 Methods comparable :: Comparable (UnderAddition t) Source # | |
| Monoid (UnderAddition Cohesion) Source # |
|
Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Cohesion Source # mappend :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion Source # mconcat :: [UnderAddition Cohesion] -> UnderAddition Cohesion Source # | |
| Monoid (UnderAddition Modality) Source # | Pointwise additive unit. |
Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Modality Source # mappend :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality Source # mconcat :: [UnderAddition Modality] -> UnderAddition Modality Source # | |
| Monoid (UnderAddition PolarityModality) Source # | '' is the additive unit. |
| Monoid (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Quantity Source # mappend :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity Source # mconcat :: [UnderAddition Quantity] -> UnderAddition Quantity Source # | |
| Monoid (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Relevance Source # mappend :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance Source # mconcat :: [UnderAddition Relevance] -> UnderAddition Relevance Source # | |
| Semigroup (UnderAddition Cohesion) Source # |
|
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion Source # sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion Source # stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion Source # | |
| Semigroup (UnderAddition Modality) Source # | Pointwise addition. |
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality Source # sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality Source # stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality Source # | |
| Semigroup (UnderAddition PolarityModality) Source # |
|
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition PolarityModality -> UnderAddition PolarityModality -> UnderAddition PolarityModality Source # sconcat :: NonEmpty (UnderAddition PolarityModality) -> UnderAddition PolarityModality Source # stimes :: Integral b => b -> UnderAddition PolarityModality -> UnderAddition PolarityModality Source # | |
| Semigroup (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity Source # sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity Source # stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity Source # | |
| Semigroup (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance Source # sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance Source # stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance Source # | |
| Show t => Show (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common | |
| Eq t => Eq (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: UnderAddition t -> UnderAddition t -> Bool Source # (/=) :: UnderAddition t -> UnderAddition t -> Bool Source # | |
| Ord t => Ord (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common Methods compare :: UnderAddition t -> UnderAddition t -> Ordering Source # (<) :: UnderAddition t -> UnderAddition t -> Bool Source # (<=) :: UnderAddition t -> UnderAddition t -> Bool Source # (>) :: UnderAddition t -> UnderAddition t -> Bool Source # (>=) :: UnderAddition t -> UnderAddition t -> Bool Source # max :: UnderAddition t -> UnderAddition t -> UnderAddition t Source # min :: UnderAddition t -> UnderAddition t -> UnderAddition t Source # | |
newtype UnderComposition t Source #
Type wrapper to indicate composition or multiplicative monoid/semigroup context.
Constructors
| UnderComposition t |
Instances
| Applicative UnderComposition Source # | |
Defined in Agda.Syntax.Common Methods pure :: a -> UnderComposition a Source # (<*>) :: UnderComposition (a -> b) -> UnderComposition a -> UnderComposition b Source # liftA2 :: (a -> b -> c) -> UnderComposition a -> UnderComposition b -> UnderComposition c Source # (*>) :: UnderComposition a -> UnderComposition b -> UnderComposition b Source # (<*) :: UnderComposition a -> UnderComposition b -> UnderComposition a Source # | |
| Functor UnderComposition Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> UnderComposition a -> UnderComposition b Source # (<$) :: a -> UnderComposition b -> UnderComposition a Source # | |
| LeftClosedPOMonoid (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion Source # | |
| LeftClosedPOMonoid (UnderComposition Modality) Source # | |
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality Source # | |
| LeftClosedPOMonoid (UnderComposition PolarityModality) Source # | |
Defined in Agda.Syntax.Common | |
| LeftClosedPOMonoid (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity Source # | |
| LeftClosedPOMonoid (UnderComposition Relevance) Source # | |
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance Source # | |
| POMonoid (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
| POMonoid (UnderComposition Modality) Source # | |
Defined in Agda.Syntax.Common | |
| POMonoid (UnderComposition PolarityModality) 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 PolarityModality) 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 Methods comparable :: Comparable (UnderComposition t) Source # | |
| Monoid (UnderComposition Cohesion) Source # |
|
Defined in Agda.Syntax.Common | |
| Monoid (UnderComposition Modality) Source # | Pointwise composition unit. |
Defined in Agda.Syntax.Common | |
| Monoid (UnderComposition PolarityModality) 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. |
Defined in Agda.Syntax.Common | |
| Monoid (UnderComposition Relevance) Source # |
|
Defined in Agda.Syntax.Common | |
| Semigroup (UnderComposition Cohesion) Source # |
|
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion Source # sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion Source # stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion Source # | |
| Semigroup (UnderComposition Erased) Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased Source # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased Source # stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased Source # | |
| Semigroup (UnderComposition Modality) Source # | Pointwise composition. |
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality Source # sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality Source # stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality Source # | |
| Semigroup (UnderComposition PolarityModality) Source # |
|
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition PolarityModality -> UnderComposition PolarityModality -> UnderComposition PolarityModality Source # sconcat :: NonEmpty (UnderComposition PolarityModality) -> UnderComposition PolarityModality Source # stimes :: Integral b => b -> UnderComposition PolarityModality -> UnderComposition PolarityModality Source # | |
| Semigroup (UnderComposition Quantity) Source # | Composition of quantities (multiplication).
Right-biased for origin. |
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity Source # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity Source # stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity Source # | |
| Semigroup (UnderComposition Relevance) Source # |
|
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance Source # sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance Source # stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance Source # | |
| Show t => Show (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common | |
| Eq t => Eq (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: UnderComposition t -> UnderComposition t -> Bool Source # (/=) :: UnderComposition t -> UnderComposition t -> Bool Source # | |
| Ord t => Ord (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common Methods compare :: UnderComposition t -> UnderComposition t -> Ordering Source # (<) :: UnderComposition t -> UnderComposition t -> Bool Source # (<=) :: UnderComposition t -> UnderComposition t -> Bool Source # (>) :: UnderComposition t -> UnderComposition t -> Bool Source # (>=) :: UnderComposition t -> UnderComposition t -> Bool Source # max :: UnderComposition t -> UnderComposition t -> UnderComposition t Source # min :: UnderComposition t -> UnderComposition t -> UnderComposition t Source # | |
Quantity for linearity.
A quantity is a set of natural numbers, indicating possible semantic
uses of a variable. A singleton set {n} requires that the
corresponding variable is used exactly n times.
Constructors
| Quantity0 Q0Origin | Zero uses |
| 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 Methods | |||||
| SetRange Quantity Source # | |||||
| Verbalize Quantity Source # | |||||
| PrettyTCM Quantity Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| EmbPrj Quantity Source # | |||||
| Unquote Quantity Source # | |||||
| Null Quantity Source # |
| ||||
| PartialOrd Quantity Source # | Note that the order is | ||||
Defined in Agda.Syntax.Common Methods | |||||
| NFData Quantity Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic Quantity Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Quantity Source # | |||||
| Eq Quantity Source # | |||||
| Ord Quantity Source # | |||||
Defined in Agda.Syntax.Common | |||||
| LeftClosedPOMonoid (UnderComposition Quantity) Source # | |||||
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity Source # | |||||
| 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 Methods mempty :: UnderAddition Quantity Source # mappend :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity Source # mconcat :: [UnderAddition Quantity] -> UnderAddition Quantity Source # | |||||
| Monoid (UnderComposition Quantity) Source # | In the absense of finite quantities besides 0, ω is the unit. Otherwise, 1 is the unit. | ||||
Defined in Agda.Syntax.Common | |||||
| Semigroup (UnderAddition Quantity) Source # | |||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity Source # sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity Source # stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity Source # | |||||
| Semigroup (UnderComposition Quantity) Source # | Composition of quantities (multiplication).
Right-biased for origin. | ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity Source # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity Source # stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity Source # | |||||
| type Rep Quantity Source # | |||||
Defined in Agda.Syntax.Common type Rep Quantity = D1 ('MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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 #
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.
usablePolarity :: LensModalPolarity a => a -> Bool Source #
usablePolarity pol == False iff we cannot use a variable of pol.
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.
composePolarity :: PolarityModality -> PolarityModality -> PolarityModality Source #
PolarityModality composition.
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.
inverseComposePolarity :: PolarityModality -> PolarityModality -> PolarityModality Source #
inverseComposePolarity r x returns the least y
such that forall x, y we have
x `morePolarity'\` (r `composePolarity` y)
iff
(r `inverseComposePolarity` x) `morePolarity'\` y (Galois connection).
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.
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.
addPolarity :: PolarityModality -> PolarityModality -> PolarityModality Source #
Combine inferred PolarityModality.
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.
zeroPolarity :: PolarityModality Source #
ModalPolarity 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
unitPolarity :: PolarityModality 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.
topPolarity :: PolarityModality 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
defaultPolarity :: PolarityModality Source #
Default used when not caring about polarity
defaultCheckModality :: Modality Source #
The default Modality terms are checked against.
data ModalPolarity Source #
The different polarity options
Constructors
| UnusedPolarity | argument will not be used. |
| StrictlyPositive | argument will only be used in strictly positive position. |
| Positive | argument will only be used in positive position. |
| Negative | argument will only be used in negative position. |
| MixedPolarity | we don't know anything, argument can be used anywhere. |
Instances
| Pretty ModalPolarity Source # | |||||
Defined in Agda.Syntax.Common Methods pretty :: ModalPolarity -> Doc Source # prettyPrec :: Int -> ModalPolarity -> Doc Source # prettyList :: [ModalPolarity] -> Doc Source # | |||||
| Verbalize ModalPolarity Source # | |||||
Defined in Agda.TypeChecking.Errors Methods verbalize :: ModalPolarity -> String Source # | |||||
| PrettyTCM ModalPolarity Source # | |||||
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ModalPolarity -> m Doc Source # | |||||
| EmbPrj ModalPolarity Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| PartialOrd ModalPolarity Source # | The derived Ord instance for ModalPolarity is just used for serialisation and has no particular meaning. The actual order on modalities is a partial order. | ||||
Defined in Agda.Syntax.Common Methods | |||||
| Bounded ModalPolarity Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum ModalPolarity Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: ModalPolarity -> ModalPolarity Source # pred :: ModalPolarity -> ModalPolarity Source # toEnum :: Int -> ModalPolarity Source # fromEnum :: ModalPolarity -> Int Source # enumFrom :: ModalPolarity -> [ModalPolarity] Source # enumFromThen :: ModalPolarity -> ModalPolarity -> [ModalPolarity] Source # enumFromTo :: ModalPolarity -> ModalPolarity -> [ModalPolarity] Source # enumFromThenTo :: ModalPolarity -> ModalPolarity -> ModalPolarity -> [ModalPolarity] Source # | |||||
| Generic ModalPolarity Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods from :: ModalPolarity -> Rep ModalPolarity x Source # to :: Rep ModalPolarity x -> ModalPolarity Source # | |||||
| Show ModalPolarity Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq ModalPolarity Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: ModalPolarity -> ModalPolarity -> Bool Source # (/=) :: ModalPolarity -> ModalPolarity -> Bool Source # | |||||
| Ord ModalPolarity Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: ModalPolarity -> ModalPolarity -> Ordering Source # (<) :: ModalPolarity -> ModalPolarity -> Bool Source # (<=) :: ModalPolarity -> ModalPolarity -> Bool Source # (>) :: ModalPolarity -> ModalPolarity -> Bool Source # (>=) :: ModalPolarity -> ModalPolarity -> Bool Source # max :: ModalPolarity -> ModalPolarity -> ModalPolarity Source # min :: ModalPolarity -> ModalPolarity -> ModalPolarity Source # | |||||
| type Rep ModalPolarity Source # | |||||
Defined in Agda.Syntax.Common type Rep ModalPolarity = D1 ('MetaData "ModalPolarity" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) ((C1 ('MetaCons "UnusedPolarity" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "StrictlyPositive" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Positive" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Negative" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MixedPolarity" 'PrefixI 'False) (U1 :: Type -> Type)))) | |||||
positionalModalityComponent :: Modality -> Modality Source #
Extract the positional modality component for checks regarding only them.
sameModality :: (LensModality a, LensModality b) => a -> b -> Bool Source #
Equality ignoring origin.
samePolarity :: PolarityModality -> PolarityModality -> Bool Source #
Equality for polarities.
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 #
getPolarityMod :: LensModality a => LensGet a PolarityModality Source #
setPolarityMod :: LensModality a => LensSet a PolarityModality Source #
mapPolarityMod :: LensModality a => LensMap a PolarityModality Source #
Origin of Quantity0.
Constructors
| 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 Methods | |||||
| 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 Associated Types
| |||||
| Show Q0Origin Source # | |||||
| Eq Q0Origin Source # | |||||
| Ord Q0Origin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type Rep Q0Origin Source # | |||||
Defined in Agda.Syntax.Common type Rep Q0Origin = D1 ('MetaData "Q0Origin" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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ω.
Constructors
| 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 Methods | |||||
| 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 Associated Types
| |||||
| Show QωOrigin Source # | |||||
| Eq QωOrigin Source # | |||||
| Ord QωOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type Rep QωOrigin Source # | |||||
Defined in Agda.Syntax.Common type Rep QωOrigin = D1 ('MetaData "Q\969Origin" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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?
isQuantity0 :: LensQuantity a => a -> Bool Source #
isQuantityω :: LensQuantity a => a -> Bool Source #
prettyQuantity :: LensQuantity a => a -> Doc -> Doc 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 Methods | |||||
| PrettyTCM Erased Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| NFData Erased Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic Erased Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Erased Source # | |||||
| Eq Erased Source # | |||||
| Ord Erased Source # | |||||
| Semigroup (UnderComposition Erased) Source # | |||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased Source # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased Source # stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased Source # | |||||
| type Rep Erased Source # | |||||
Defined in Agda.Syntax.Common type Rep Erased = D1 ('MetaData "Erased" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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.
data OriginRelevant Source #
Origin of Relevant.
Constructors
| ORelInferred | User wrote nothing. |
| ORelRelevant Range | User wrote "@relevant". |
Instances
| Pretty OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common Methods pretty :: OriginRelevant -> Doc Source # prettyPrec :: Int -> OriginRelevant -> Doc Source # prettyList :: [OriginRelevant] -> Doc Source # | |||||
| HasRange OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common Methods getRange :: OriginRelevant -> Range Source # | |||||
| KillRange OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| SetRange OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common Methods setRange :: Range -> OriginRelevant -> OriginRelevant Source # | |||||
| EmbPrj OriginRelevant Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| Null OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common | |||||
| NFData OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: OriginRelevant -> () Source # | |||||
| Monoid OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common Methods mempty :: OriginRelevant Source # mappend :: OriginRelevant -> OriginRelevant -> OriginRelevant Source # mconcat :: [OriginRelevant] -> OriginRelevant Source # | |||||
| Semigroup OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common Methods (<>) :: OriginRelevant -> OriginRelevant -> OriginRelevant Source # sconcat :: NonEmpty OriginRelevant -> OriginRelevant Source # stimes :: Integral b => b -> OriginRelevant -> OriginRelevant Source # | |||||
| Generic OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods from :: OriginRelevant -> Rep OriginRelevant x Source # to :: Rep OriginRelevant x -> OriginRelevant Source # | |||||
| Show OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type Rep OriginRelevant Source # | |||||
Defined in Agda.Syntax.Common type Rep OriginRelevant = D1 ('MetaData "OriginRelevant" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) (C1 ('MetaCons "ORelInferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ORelRelevant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) | |||||
data OriginIrrelevant Source #
Origin of Irrelevant.
Constructors
| OIrrInferred | User wrote nothing. |
| OIrrDot Range | User wrote ".". |
| OIrrIrr Range | User wrote "@irr". |
| OIrrIrrelevant Range | User wrote "@irrelevant". |
Instances
| Pretty OriginIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods pretty :: OriginIrrelevant -> Doc Source # prettyPrec :: Int -> OriginIrrelevant -> Doc Source # prettyList :: [OriginIrrelevant] -> Doc Source # | |||||
| HasRange OriginIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods getRange :: OriginIrrelevant -> Range Source # | |||||
| KillRange OriginIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| SetRange OriginIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods setRange :: Range -> OriginIrrelevant -> OriginIrrelevant Source # | |||||
| EmbPrj OriginIrrelevant Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| Null OriginIrrelevant Source # | |||||
Defined in Agda.Syntax.Common | |||||
| NFData OriginIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: OriginIrrelevant -> () Source # | |||||
| Monoid OriginIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods mempty :: OriginIrrelevant Source # mappend :: OriginIrrelevant -> OriginIrrelevant -> OriginIrrelevant Source # mconcat :: [OriginIrrelevant] -> OriginIrrelevant Source # | |||||
| Semigroup OriginIrrelevant Source # | Right-biased composition, because the left relevance acts as context, and the right one as occurrence. | ||||
Defined in Agda.Syntax.Common Methods (<>) :: OriginIrrelevant -> OriginIrrelevant -> OriginIrrelevant Source # sconcat :: NonEmpty OriginIrrelevant -> OriginIrrelevant Source # stimes :: Integral b => b -> OriginIrrelevant -> OriginIrrelevant Source # | |||||
| Generic OriginIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods from :: OriginIrrelevant -> Rep OriginIrrelevant x Source # to :: Rep OriginIrrelevant x -> OriginIrrelevant Source # | |||||
| Show OriginIrrelevant Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type Rep OriginIrrelevant Source # | |||||
Defined in Agda.Syntax.Common type Rep OriginIrrelevant = D1 ('MetaData "OriginIrrelevant" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) ((C1 ('MetaCons "OIrrInferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OIrrDot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "OIrrIrr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "OIrrIrrelevant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |||||
data OriginShapeIrrelevant Source #
Origin of ShapeIrrelevant.
Constructors
| OShIrrInferred | User wrote nothing. |
| OShIrrDotDot Range | User wrote "..". |
| OShIrrShIrr Range | User wrote "@shirr". |
| OShIrrShapeIrrelevant Range | User wrote "@shape-irrelevant". |
Instances
| Pretty OriginShapeIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods pretty :: OriginShapeIrrelevant -> Doc Source # prettyPrec :: Int -> OriginShapeIrrelevant -> Doc Source # prettyList :: [OriginShapeIrrelevant] -> Doc Source # | |||||
| HasRange OriginShapeIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| KillRange OriginShapeIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| SetRange OriginShapeIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods setRange :: Range -> OriginShapeIrrelevant -> OriginShapeIrrelevant Source # | |||||
| EmbPrj OriginShapeIrrelevant Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| Null OriginShapeIrrelevant Source # | |||||
Defined in Agda.Syntax.Common | |||||
| NFData OriginShapeIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: OriginShapeIrrelevant -> () Source # | |||||
| Monoid OriginShapeIrrelevant Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Semigroup OriginShapeIrrelevant Source # | Right-biased composition, because the left relevance acts as context, and the right one as occurrence. | ||||
Defined in Agda.Syntax.Common Methods (<>) :: OriginShapeIrrelevant -> OriginShapeIrrelevant -> OriginShapeIrrelevant Source # sconcat :: NonEmpty OriginShapeIrrelevant -> OriginShapeIrrelevant Source # stimes :: Integral b => b -> OriginShapeIrrelevant -> OriginShapeIrrelevant Source # | |||||
| Generic OriginShapeIrrelevant Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods from :: OriginShapeIrrelevant -> Rep OriginShapeIrrelevant x Source # to :: Rep OriginShapeIrrelevant x -> OriginShapeIrrelevant Source # | |||||
| Show OriginShapeIrrelevant Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type Rep OriginShapeIrrelevant Source # | |||||
Defined in Agda.Syntax.Common type Rep OriginShapeIrrelevant = D1 ('MetaData "OriginShapeIrrelevant" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) ((C1 ('MetaCons "OShIrrInferred" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OShIrrDotDot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "OShIrrShIrr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "OShIrrShapeIrrelevant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |||||
isRelevant :: LensRelevance a => a -> Bool Source #
isIrrelevant :: LensRelevance a => a -> Bool Source #
isShapeIrrelevant :: LensRelevance a => a -> Bool Source #
moreRelevant :: Relevance -> Relevance -> Bool Source #
Information ordering.
Relevant `moreRelevant`
ShapeIrrelevant `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.
irrelevantToShapeIrrelevant :: Relevance -> Relevance Source #
Irrelevant function arguments may appear non-strictly in the codomain type.
shapeIrrelevantToRelevant :: Relevance -> Relevance Source #
Applied when working on types (unless --experimental-irrelevance).
prettyRelevance :: LensRelevance a => a -> Doc -> Doc Source #
data Annotation Source #
We have a tuple of annotations, which might not be fully orthogonal.
Constructors
| Annotation | |
Instances
| LensAnnotation Annotation Source # | |||||
Defined in Agda.Syntax.Common Methods getAnnotation :: Annotation -> Annotation Source # setAnnotation :: Annotation -> Annotation -> Annotation Source # mapAnnotation :: (Annotation -> Annotation) -> Annotation -> Annotation Source # | |||||
| HasRange Annotation Source # | |||||
Defined in Agda.Syntax.Common Methods getRange :: Annotation -> Range Source # | |||||
| KillRange Annotation Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| EmbPrj Annotation Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| Null Annotation Source # | |||||
Defined in Agda.Syntax.Common | |||||
| NFData Annotation Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: Annotation -> () Source # | |||||
| Generic Annotation Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Annotation Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq Annotation Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: Annotation -> Annotation -> Bool Source # (/=) :: Annotation -> Annotation -> Bool Source # | |||||
| Ord Annotation Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: Annotation -> Annotation -> Ordering Source # (<) :: Annotation -> Annotation -> Bool Source # (<=) :: Annotation -> Annotation -> Bool Source # (>) :: Annotation -> Annotation -> Bool Source # (>=) :: Annotation -> Annotation -> Bool Source # max :: Annotation -> Annotation -> Annotation Source # min :: Annotation -> Annotation -> Annotation Source # | |||||
| type Rep Annotation Source # | |||||
Defined in Agda.Syntax.Common type Rep Annotation = D1 ('MetaData "Annotation" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) (C1 ('MetaCons "Annotation" 'PrefixI 'True) (S1 ('MetaSel ('Just "annLock") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lock))) | |||||
defaultLock :: Lock Source #
class LensAnnotation a where Source #
Minimal complete definition
Nothing
Methods
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 Methods getAnnotation :: Annotation -> Annotation Source # setAnnotation :: Annotation -> Annotation -> Annotation Source # mapAnnotation :: (Annotation -> Annotation) -> Annotation -> Annotation Source # | |
| LensAnnotation ArgInfo Source # | |
Defined in Agda.Syntax.Common Methods getAnnotation :: ArgInfo -> Annotation Source # setAnnotation :: Annotation -> ArgInfo -> ArgInfo Source # mapAnnotation :: (Annotation -> Annotation) -> ArgInfo -> ArgInfo Source # | |
| LensAnnotation (Arg t) Source # | |
Defined in Agda.Syntax.Common Methods 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 Methods 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 Methods succ :: LockOrigin -> LockOrigin Source # pred :: LockOrigin -> LockOrigin Source # toEnum :: Int -> LockOrigin Source # fromEnum :: LockOrigin -> Int Source # enumFrom :: LockOrigin -> [LockOrigin] Source # enumFromThen :: LockOrigin -> LockOrigin -> [LockOrigin] Source # enumFromTo :: LockOrigin -> LockOrigin -> [LockOrigin] Source # enumFromThenTo :: LockOrigin -> LockOrigin -> LockOrigin -> [LockOrigin] Source # | |||||
| Generic LockOrigin Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show LockOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq LockOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: LockOrigin -> LockOrigin -> Bool Source # (/=) :: LockOrigin -> LockOrigin -> Bool Source # | |||||
| Ord LockOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: LockOrigin -> LockOrigin -> Ordering Source # (<) :: LockOrigin -> LockOrigin -> Bool Source # (<=) :: LockOrigin -> LockOrigin -> Bool Source # (>) :: LockOrigin -> LockOrigin -> Bool Source # (>=) :: LockOrigin -> LockOrigin -> Bool Source # max :: LockOrigin -> LockOrigin -> LockOrigin Source # min :: LockOrigin -> LockOrigin -> LockOrigin Source # | |||||
| type Rep LockOrigin Source # | |||||
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.
prettyCohesion :: LensCohesion a => a -> Doc -> Doc Source #
morePolarity' :: ModalPolarity -> ModalPolarity -> Bool Source #
morePolarity' x y is True whenever a variable of polarity x can be
used anywhere where a variable of polarity y is expected.
Note that morePolarity' x y actually means x <= y.
splittablePolarity :: LensModalPolarity a => a -> Bool Source #
splittablePolarity pol == False iff we cannot split on a variable of pol.
composePolarity' :: ModalPolarity -> ModalPolarity -> ModalPolarity Source #
ModalPolarity composition.
UnusedPolarity is dominant, StrictlyPositive is neutral.
inverseComposePolarity' :: ModalPolarity -> ModalPolarity -> ModalPolarity Source #
inverseComposePolarity r x returns the least y
such that forall x, y we have
x `morePolarity'\` (r `composePolarity` y)
iff
(r `inverseComposePolarity` x) `morePolarity'\` y (Galois connection).
addPolarity' :: ModalPolarity -> ModalPolarity -> ModalPolarity Source #
Combine inferred ModalPolarity.
The unit is UnusedPolarity.
morePolarity :: PolarityModality -> PolarityModality -> Bool Source #
applyPolarity :: LensModalPolarity a => PolarityModality -> a -> a Source #
Compose with polarity flag from the left.
This function is e.g. used to update the polarity information
on pattern variables a after a match against something of polarity pol.
inverseApplyPolarity :: LensModalPolarity a => PolarityModality -> a -> a Source #
Left division by a PolarityModality.
Used e.g. to modify context when going into a pol argument.
negativePolarity :: PolarityModality Source #
Alias for Negative polarity.
mixedPolarity :: PolarityModality Source #
Alias for Mixed polarity.
prettyPolarity :: LensModalPolarity a => a -> Doc -> Doc Source #
data BinderNameOrigin Source #
Constructors
| UserBinderName | |
| InsertedBinderName |
Instances
| KillRange BinderNameOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| NFData BinderNameOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: BinderNameOrigin -> () Source # | |||||
| Generic BinderNameOrigin Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods from :: BinderNameOrigin -> Rep BinderNameOrigin x Source # to :: Rep BinderNameOrigin x -> BinderNameOrigin Source # | |||||
| Show BinderNameOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq BinderNameOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: BinderNameOrigin -> BinderNameOrigin -> Bool Source # (/=) :: BinderNameOrigin -> BinderNameOrigin -> Bool Source # | |||||
| type Rep BinderNameOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
data FreeVariables Source #
Constructors
| UnknownFVs | |
| KnownFVs IntSet |
Instances
| LensFreeVariables FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods getFreeVariables :: FreeVariables -> FreeVariables Source # setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables Source # | |
| KillRange FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods | |
| EmbPrj FreeVariables Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| NFData FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods rnf :: FreeVariables -> () Source # | |
| Monoid FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods mempty :: FreeVariables Source # mappend :: FreeVariables -> FreeVariables -> FreeVariables Source # mconcat :: [FreeVariables] -> FreeVariables Source # | |
| Semigroup FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: FreeVariables -> FreeVariables -> FreeVariables Source # sconcat :: NonEmpty FreeVariables -> FreeVariables Source # stimes :: Integral b => b -> FreeVariables -> FreeVariables Source # | |
| Show FreeVariables Source # | |
Defined in Agda.Syntax.Common | |
| Eq FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods (==) :: FreeVariables -> FreeVariables -> Bool Source # (/=) :: FreeVariables -> FreeVariables -> Bool Source # | |
| Ord FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods compare :: FreeVariables -> FreeVariables -> Ordering Source # (<) :: FreeVariables -> FreeVariables -> Bool Source # (<=) :: FreeVariables -> FreeVariables -> Bool Source # (>) :: FreeVariables -> FreeVariables -> Bool Source # (>=) :: FreeVariables -> FreeVariables -> Bool Source # max :: FreeVariables -> FreeVariables -> FreeVariables Source # min :: FreeVariables -> FreeVariables -> FreeVariables Source # | |
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.
Minimal complete definition
Nothing
Methods
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 Methods getFreeVariables :: ArgInfo -> FreeVariables Source # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo Source # | |
| LensFreeVariables FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods getFreeVariables :: FreeVariables -> FreeVariables Source # setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables Source # | |
| LensFreeVariables (Arg e) Source # | |
Defined in Agda.Syntax.Common Methods 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 Methods 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 #
defaultArg :: a -> Arg a Source #
withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] Source #
class Eq a => Underscore a where Source #
Minimal complete definition
Instances
| Underscore Expr Source # | |
Defined in Agda.Syntax.Abstract | |
| Underscore Doc Source # | |
Defined in Agda.Syntax.Common | |
| Underscore Name Source # | |
Defined in Agda.Syntax.Concrete.Name | |
| Underscore QName Source # | |
Defined in Agda.Syntax.Concrete.Name | |
| Underscore ByteString Source # | |
Defined in Agda.Syntax.Common | |
| Underscore String Source # | |
Defined in Agda.Syntax.Common | |
class LensNamed a where Source #
Accessor/editor for the nameOf component.
Minimal complete definition
Nothing
Methods
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.
Instances
| Show IsInfix Source # | |
| Eq IsInfix Source # | |
| Ord IsInfix Source # | |
Defined in Agda.Syntax.Common | |
Access modifier.
Constructors
| PrivateAccess KwRange Origin | Store the |
| PublicAccess |
Instances
| Pretty Access Source # | |
| HasRange Access Source # | |
| KillRange Access Source # | |
Defined in Agda.Syntax.Common Methods | |
| EmbPrj Access Source # | |
| NFData Access Source # | |
Defined in Agda.Syntax.Common | |
| Show Access Source # | |
| Eq Access Source # | |
| Ord Access Source # | |
data IsAbstract Source #
Abstract or concrete.
Constructors
| AbstractDef | |
| ConcreteDef |
Instances
| AnyIsAbstract IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Methods anyIsAbstract :: IsAbstract -> IsAbstract Source # | |||||
| LensIsAbstract IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| KillRange IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| EmbPrj IsAbstract Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| Boolean IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Methods 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 Methods 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 Methods rnf :: IsAbstract -> () Source # | |||||
| Monoid IsAbstract Source # | Default is | ||||
Defined in Agda.Syntax.Common Methods mempty :: IsAbstract Source # mappend :: IsAbstract -> IsAbstract -> IsAbstract Source # mconcat :: [IsAbstract] -> IsAbstract Source # | |||||
| Semigroup IsAbstract Source # | Semigroup computes if any of several is an | ||||
Defined in Agda.Syntax.Common Methods (<>) :: IsAbstract -> IsAbstract -> IsAbstract Source # sconcat :: NonEmpty IsAbstract -> IsAbstract Source # stimes :: Integral b => b -> IsAbstract -> IsAbstract Source # | |||||
| Generic IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show IsAbstract Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: IsAbstract -> IsAbstract -> Bool Source # (/=) :: IsAbstract -> IsAbstract -> Bool Source # | |||||
| Ord IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: IsAbstract -> IsAbstract -> Ordering Source # (<) :: IsAbstract -> IsAbstract -> Bool Source # (<=) :: IsAbstract -> IsAbstract -> Bool Source # (>) :: IsAbstract -> IsAbstract -> Bool Source # (>=) :: IsAbstract -> IsAbstract -> Bool Source # max :: IsAbstract -> IsAbstract -> IsAbstract Source # min :: IsAbstract -> IsAbstract -> IsAbstract Source # | |||||
| type Rep IsAbstract Source # | |||||
class LensIsAbstract a where Source #
Methods
lensIsAbstract :: Lens' a IsAbstract Source #
Instances
| LensIsAbstract IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods | |
| LensIsAbstract MetaInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| LensIsAbstract TCEnv Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| LensIsAbstract (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods lensIsAbstract :: Lens' (DefInfo' t) IsAbstract Source # | |
| LensIsAbstract (Closure a) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods lensIsAbstract :: Lens' (Closure a) IsAbstract Source # | |
class AnyIsAbstract a where Source #
Is any element of a collection an AbstractDef.
Minimal complete definition
Nothing
Methods
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 Methods anyIsAbstract :: IsAbstract -> IsAbstract Source # | |
| AnyIsAbstract (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods anyIsAbstract :: DefInfo' t -> IsAbstract Source # | |
| AnyIsAbstract a => AnyIsAbstract (Maybe a) Source # | |
Defined in Agda.Syntax.Common Methods anyIsAbstract :: Maybe a -> IsAbstract Source # | |
| AnyIsAbstract a => AnyIsAbstract [a] Source # | |
Defined in Agda.Syntax.Common Methods anyIsAbstract :: [a] -> IsAbstract Source # | |
data IsInstance Source #
Is this definition eligible for instance search?
Constructors
| InstanceDef KwRange | Range of the |
| NotInstanceDef |
Instances
| HasRange IsInstance Source # | |
Defined in Agda.Syntax.Common Methods getRange :: IsInstance -> Range Source # | |
| KillRange IsInstance Source # | |
Defined in Agda.Syntax.Common Methods | |
| EmbPrj IsInstance Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| NFData IsInstance Source # | |
Defined in Agda.Syntax.Common Methods rnf :: IsInstance -> () Source # | |
| Show IsInstance Source # | |
Defined in Agda.Syntax.Common | |
| Eq IsInstance Source # | |
Defined in Agda.Syntax.Common Methods (==) :: IsInstance -> IsInstance -> Bool Source # (/=) :: IsInstance -> IsInstance -> Bool Source # | |
| Ord IsInstance Source # | |
Defined in Agda.Syntax.Common Methods compare :: IsInstance -> IsInstance -> Ordering Source # (<) :: IsInstance -> IsInstance -> Bool Source # (<=) :: IsInstance -> IsInstance -> Bool Source # (>) :: IsInstance -> IsInstance -> Bool Source # (>=) :: IsInstance -> IsInstance -> Bool Source # max :: IsInstance -> IsInstance -> IsInstance Source # min :: IsInstance -> IsInstance -> IsInstance Source # | |
Is this a macro definition?
Constructors
| MacroDef | |
| NotMacroDef |
Instances
| HasRange IsMacro Source # | |
| KillRange IsMacro Source # | |
Defined in Agda.Syntax.Common Methods | |
| 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 # | |
Defined in Agda.Syntax.Common | |
| type Rep IsMacro Source # | |
The unique identifier of an opaque block. Second argument is the top-level module identifier.
Constructors
| OpaqueId !Word64 !ModuleNameHash |
Instances
| Pretty OpaqueId Source # | |||||
| KillRange OpaqueId Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| HasFresh OpaqueId Source # | |||||
| EmbPrj OpaqueId Source # | |||||
| NFData OpaqueId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum OpaqueId Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: OpaqueId -> OpaqueId Source # pred :: OpaqueId -> OpaqueId Source # toEnum :: Int -> OpaqueId Source # fromEnum :: OpaqueId -> Int Source # enumFrom :: OpaqueId -> [OpaqueId] Source # enumFromThen :: OpaqueId -> OpaqueId -> [OpaqueId] Source # enumFromTo :: OpaqueId -> OpaqueId -> [OpaqueId] Source # enumFromThenTo :: OpaqueId -> OpaqueId -> OpaqueId -> [OpaqueId] Source # | |||||
| Generic OpaqueId Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show OpaqueId Source # | |||||
| Eq OpaqueId Source # | |||||
| Ord OpaqueId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Hashable OpaqueId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type Rep OpaqueId Source # | |||||
Defined in Agda.Syntax.Common type Rep OpaqueId = D1 ('MetaData "OpaqueId" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" '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 #
Methods
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.
Constructors
| UniqueOpaque !OpaqueId | Every definition agrees on what opaque block they belong to. |
| DifferentOpaque !(HashSet OpaqueId) | More than one opaque block was found. |
| NoOpaque | Nothing here is opaque. |
Instances
| Monoid JointOpacity Source # | |
Defined in Agda.Syntax.Common Methods mempty :: JointOpacity Source # mappend :: JointOpacity -> JointOpacity -> JointOpacity Source # mconcat :: [JointOpacity] -> JointOpacity Source # | |
| Semigroup JointOpacity Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: JointOpacity -> JointOpacity -> JointOpacity Source # sconcat :: NonEmpty JointOpacity -> JointOpacity Source # stimes :: Integral b => b -> JointOpacity -> JointOpacity Source # | |
class AllAreOpaque a where Source #
Minimal complete definition
Nothing
Methods
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 Methods jointOpacity :: IsOpaque -> JointOpacity Source # | |
| AllAreOpaque (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods jointOpacity :: DefInfo' t -> JointOpacity Source # | |
| AllAreOpaque a => AllAreOpaque (Maybe a) Source # | |
Defined in Agda.Syntax.Common Methods jointOpacity :: Maybe a -> JointOpacity Source # | |
| AllAreOpaque a => AllAreOpaque [a] Source # | |
Defined in Agda.Syntax.Common Methods jointOpacity :: [a] -> JointOpacity Source # | |
data MaybePlaceholder e Source #
Placeholders are used to represent the underscores in a section.
Constructors
| Placeholder !PositionInName | |
| NoPlaceholder !(Maybe PositionInName) e | The second argument is used only (but not always) for name parts other than underscores. |
Instances
| Functor MaybePlaceholder Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b Source # (<$) :: a -> MaybePlaceholder b -> MaybePlaceholder a Source # | |
| Foldable MaybePlaceholder Source # | |
Defined in Agda.Syntax.Common Methods fold :: Monoid m => MaybePlaceholder m -> m Source # foldMap :: Monoid m => (a -> m) -> MaybePlaceholder a -> m Source # foldMap' :: Monoid m => (a -> m) -> MaybePlaceholder a -> m Source # foldr :: (a -> b -> b) -> b -> MaybePlaceholder a -> b Source # foldr' :: (a -> b -> b) -> b -> MaybePlaceholder a -> b Source # foldl :: (b -> a -> b) -> b -> MaybePlaceholder a -> b Source # foldl' :: (b -> a -> b) -> b -> MaybePlaceholder a -> b Source # foldr1 :: (a -> a -> a) -> MaybePlaceholder a -> a Source # foldl1 :: (a -> a -> a) -> MaybePlaceholder a -> a Source # toList :: MaybePlaceholder a -> [a] Source # null :: MaybePlaceholder a -> Bool Source # length :: MaybePlaceholder a -> Int Source # elem :: Eq a => a -> MaybePlaceholder a -> Bool Source # maximum :: Ord a => MaybePlaceholder a -> a Source # minimum :: Ord a => MaybePlaceholder a -> a Source # sum :: Num a => MaybePlaceholder a -> a Source # product :: Num a => MaybePlaceholder a -> a Source # | |
| Traversable MaybePlaceholder Source # | |
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> MaybePlaceholder a -> f (MaybePlaceholder b) Source # sequenceA :: Applicative f => MaybePlaceholder (f a) -> f (MaybePlaceholder a) Source # mapM :: Monad m => (a -> m b) -> MaybePlaceholder a -> m (MaybePlaceholder b) Source # sequence :: Monad m => MaybePlaceholder (m a) -> m (MaybePlaceholder a) Source # | |
| Pretty a => Pretty (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods 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 Methods 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 Methods getRange :: MaybePlaceholder a -> Range Source # | |
| KillRange a => KillRange (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (MaybePlaceholder a) Source # | |
| NFData a => NFData (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Common Methods rnf :: MaybePlaceholder a -> () Source # | |
| Show e => Show (MaybePlaceholder e) Source # | |
Defined in Agda.Syntax.Common | |
| Eq e => Eq (MaybePlaceholder e) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source # (/=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source # | |
| Ord e => Ord (MaybePlaceholder e) Source # | |
Defined in Agda.Syntax.Common Methods compare :: MaybePlaceholder e -> MaybePlaceholder e -> Ordering Source # (<) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source # (<=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source # (>) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source # (>=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source # max :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e Source # min :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e Source # | |
noPlaceholder :: e -> MaybePlaceholder e Source #
An abbreviation: noPlaceholder = .NoPlaceholder
Nothing
type PrecedenceLevel = Double Source #
Precedence levels for operators.
data FixityLevel Source #
Constructors
| Unrelated | No fixity declared. |
| Related !PrecedenceLevel | Fixity level declared as the number. |
Instances
| Pretty FixityLevel Source # | |
Defined in Agda.Syntax.Common Methods 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 | |
| Null FixityLevel Source # | |
Defined in Agda.Syntax.Common | |
| NFData FixityLevel Source # | |
Defined in Agda.Syntax.Common Methods rnf :: FixityLevel -> () Source # | |
| Show FixityLevel Source # | |
Defined in Agda.Syntax.Common | |
| Eq FixityLevel Source # | |
Defined in Agda.Syntax.Common Methods (==) :: FixityLevel -> FixityLevel -> Bool Source # (/=) :: FixityLevel -> FixityLevel -> Bool Source # | |
| Ord FixityLevel Source # | |
Defined in Agda.Syntax.Common Methods compare :: FixityLevel -> FixityLevel -> Ordering Source # (<) :: FixityLevel -> FixityLevel -> Bool Source # (<=) :: FixityLevel -> FixityLevel -> Bool Source # (>) :: FixityLevel -> FixityLevel -> Bool Source # (>=) :: FixityLevel -> FixityLevel -> Bool Source # max :: FixityLevel -> FixityLevel -> FixityLevel Source # min :: FixityLevel -> FixityLevel -> FixityLevel Source # | |
The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.
Constructors
| Fixity' | |
Fields
| |
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 Methods | |
| 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 #
Methods
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 Methods | |
| LensFixity AbstractName Source # | |
Defined in Agda.Syntax.Scope.Base Methods | |
| LensFixity (ThingWithFixity a) Source # | |
Defined in Agda.Syntax.Fixity Methods lensFixity :: Lens' (ThingWithFixity a) Fixity Source # | |
class LensFixity' a where Source #
Methods
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 Methods 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).
Constructors
| YesPositivityCheck | |
| NoPositivityCheck |
Instances
| KillRange PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| NFData PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: PositivityCheck -> () Source # | |||||
| Monoid PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods mempty :: PositivityCheck Source # mappend :: PositivityCheck -> PositivityCheck -> PositivityCheck Source # mconcat :: [PositivityCheck] -> PositivityCheck Source # | |||||
| Semigroup PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods (<>) :: PositivityCheck -> PositivityCheck -> PositivityCheck Source # sconcat :: NonEmpty PositivityCheck -> PositivityCheck Source # stimes :: Integral b => b -> PositivityCheck -> PositivityCheck Source # | |||||
| Bounded PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: PositivityCheck -> PositivityCheck Source # pred :: PositivityCheck -> PositivityCheck Source # toEnum :: Int -> PositivityCheck Source # fromEnum :: PositivityCheck -> Int Source # enumFrom :: PositivityCheck -> [PositivityCheck] Source # enumFromThen :: PositivityCheck -> PositivityCheck -> [PositivityCheck] Source # enumFromTo :: PositivityCheck -> PositivityCheck -> [PositivityCheck] Source # enumFromThenTo :: PositivityCheck -> PositivityCheck -> PositivityCheck -> [PositivityCheck] Source # | |||||
| Generic PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods from :: PositivityCheck -> Rep PositivityCheck x Source # to :: Rep PositivityCheck x -> PositivityCheck Source # | |||||
| Show PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: PositivityCheck -> PositivityCheck -> Bool Source # (/=) :: PositivityCheck -> PositivityCheck -> Bool Source # | |||||
| Ord PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: PositivityCheck -> PositivityCheck -> Ordering Source # (<) :: PositivityCheck -> PositivityCheck -> Bool Source # (<=) :: PositivityCheck -> PositivityCheck -> Bool Source # (>) :: PositivityCheck -> PositivityCheck -> Bool Source # (>=) :: PositivityCheck -> PositivityCheck -> Bool Source # max :: PositivityCheck -> PositivityCheck -> PositivityCheck Source # min :: PositivityCheck -> PositivityCheck -> PositivityCheck Source # | |||||
| type Rep PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
data UniverseCheck Source #
Universe check? (Default is yes).
Constructors
| YesUniverseCheck | |
| NoUniverseCheck |
Instances
| KillRange UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| NFData UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: UniverseCheck -> () Source # | |||||
| Bounded UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: UniverseCheck -> UniverseCheck Source # pred :: UniverseCheck -> UniverseCheck Source # toEnum :: Int -> UniverseCheck Source # fromEnum :: UniverseCheck -> Int Source # enumFrom :: UniverseCheck -> [UniverseCheck] Source # enumFromThen :: UniverseCheck -> UniverseCheck -> [UniverseCheck] Source # enumFromTo :: UniverseCheck -> UniverseCheck -> [UniverseCheck] Source # enumFromThenTo :: UniverseCheck -> UniverseCheck -> UniverseCheck -> [UniverseCheck] Source # | |||||
| Generic UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods from :: UniverseCheck -> Rep UniverseCheck x Source # to :: Rep UniverseCheck x -> UniverseCheck Source # | |||||
| Show UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: UniverseCheck -> UniverseCheck -> Bool Source # (/=) :: UniverseCheck -> UniverseCheck -> Bool Source # | |||||
| Ord UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: UniverseCheck -> UniverseCheck -> Ordering Source # (<) :: UniverseCheck -> UniverseCheck -> Bool Source # (<=) :: UniverseCheck -> UniverseCheck -> Bool Source # (>) :: UniverseCheck -> UniverseCheck -> Bool Source # (>=) :: UniverseCheck -> UniverseCheck -> Bool Source # max :: UniverseCheck -> UniverseCheck -> UniverseCheck Source # min :: UniverseCheck -> UniverseCheck -> UniverseCheck Source # | |||||
| type Rep UniverseCheck Source # | |||||
Constructors
| YesCatchall Range | |
| NoCatchall |
Instances
| KillRange Catchall Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| EmbPrj Catchall Source # | |||||
| Null Catchall Source # | |||||
| NFData Catchall Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Monoid Catchall Source # | |||||
| Semigroup Catchall Source # | Composition is left-biased, taking the left | ||||
| Generic Catchall Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Catchall Source # | |||||
| Eq Catchall Source # | |||||
| type Rep Catchall Source # | |||||
Defined in Agda.Syntax.Common type Rep Catchall = D1 ('MetaData "Catchall" "Agda.Syntax.Common" "Agda-2.8.0-18SVM2g5zyJD8D0Ly2N2tb" 'False) (C1 ('MetaCons "YesCatchall" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "NoCatchall" 'PrefixI 'False) (U1 :: Type -> Type)) | |||||
data CoverageCheck Source #
Coverage check? (Default is yes).
Constructors
| YesCoverageCheck | |
| NoCoverageCheck |
Instances
| KillRange CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| NFData CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: CoverageCheck -> () Source # | |||||
| Monoid CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods mempty :: CoverageCheck Source # mappend :: CoverageCheck -> CoverageCheck -> CoverageCheck Source # mconcat :: [CoverageCheck] -> CoverageCheck Source # | |||||
| Semigroup CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods (<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck Source # sconcat :: NonEmpty CoverageCheck -> CoverageCheck Source # stimes :: Integral b => b -> CoverageCheck -> CoverageCheck Source # | |||||
| Bounded CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: CoverageCheck -> CoverageCheck Source # pred :: CoverageCheck -> CoverageCheck Source # toEnum :: Int -> CoverageCheck Source # fromEnum :: CoverageCheck -> Int Source # enumFrom :: CoverageCheck -> [CoverageCheck] Source # enumFromThen :: CoverageCheck -> CoverageCheck -> [CoverageCheck] Source # enumFromTo :: CoverageCheck -> CoverageCheck -> [CoverageCheck] Source # enumFromThenTo :: CoverageCheck -> CoverageCheck -> CoverageCheck -> [CoverageCheck] Source # | |||||
| Generic CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods from :: CoverageCheck -> Rep CoverageCheck x Source # to :: Rep CoverageCheck x -> CoverageCheck Source # | |||||
| Show CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: CoverageCheck -> CoverageCheck -> Bool Source # (/=) :: CoverageCheck -> CoverageCheck -> Bool Source # | |||||
| Ord CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: CoverageCheck -> CoverageCheck -> Ordering Source # (<) :: CoverageCheck -> CoverageCheck -> Bool Source # (<=) :: CoverageCheck -> CoverageCheck -> Bool Source # (>) :: CoverageCheck -> CoverageCheck -> Bool Source # (>=) :: CoverageCheck -> CoverageCheck -> Bool Source # max :: CoverageCheck -> CoverageCheck -> CoverageCheck Source # min :: CoverageCheck -> CoverageCheck -> CoverageCheck Source # | |||||
| type Rep CoverageCheck Source # | |||||
data ExpandedEllipsis Source #
Constructors
| ExpandedEllipsis | |
Fields | |
| NoEllipsis | |
Instances
| KillRange ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods | |
| EmbPrj ExpandedEllipsis Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| Null ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common | |
| NFData ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods rnf :: ExpandedEllipsis -> () Source # | |
| Monoid ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods mempty :: ExpandedEllipsis Source # mappend :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis Source # mconcat :: [ExpandedEllipsis] -> ExpandedEllipsis Source # | |
| Semigroup ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis Source # sconcat :: NonEmpty ExpandedEllipsis -> ExpandedEllipsis Source # stimes :: Integral b => b -> ExpandedEllipsis -> ExpandedEllipsis Source # | |
| Show ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common | |
| Eq ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods (==) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool Source # (/=) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool Source # | |
data NotationPart Source #
Notation parts.
Constructors
| 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 Methods pretty :: NotationPart -> Doc Source # prettyPrec :: Int -> NotationPart -> Doc Source # prettyList :: [NotationPart] -> Doc Source # | |
| HasRange NotationPart Source # | |
Defined in Agda.Syntax.Common Methods getRange :: NotationPart -> Range Source # | |
| KillRange NotationPart Source # | |
Defined in Agda.Syntax.Common Methods | |
| SetRange NotationPart Source # | |
Defined in Agda.Syntax.Common Methods setRange :: Range -> NotationPart -> NotationPart Source # | |
| EmbPrj NotationPart Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| NFData NotationPart Source # | |
Defined in Agda.Syntax.Common Methods rnf :: NotationPart -> () Source # | |
| Show NotationPart Source # | |
Defined in Agda.Syntax.Common | |
| Eq NotationPart Source # | |
Defined in Agda.Syntax.Common Methods (==) :: NotationPart -> NotationPart -> Bool Source # (/=) :: NotationPart -> NotationPart -> Bool Source # | |
| Ord NotationPart Source # | |
Defined in Agda.Syntax.Common Methods compare :: NotationPart -> NotationPart -> Ordering Source # (<) :: NotationPart -> NotationPart -> Bool Source # (<=) :: NotationPart -> NotationPart -> Bool Source # (>) :: NotationPart -> NotationPart -> Bool Source # (>=) :: NotationPart -> NotationPart -> Bool Source # max :: NotationPart -> NotationPart -> NotationPart Source # min :: NotationPart -> NotationPart -> NotationPart Source # | |
data BoundVariablePosition Source #
Positions of variables in syntax declarations.
Constructors
| BoundVariablePosition | |
Fields
| |
Instances
| EmbPrj BoundVariablePosition Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| NFData BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common Methods rnf :: BoundVariablePosition -> () Source # | |
| Show BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common | |
| Eq BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common Methods (==) :: BoundVariablePosition -> BoundVariablePosition -> Bool Source # (/=) :: BoundVariablePosition -> BoundVariablePosition -> Bool Source # | |
| Ord BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common Methods compare :: BoundVariablePosition -> BoundVariablePosition -> Ordering Source # (<) :: BoundVariablePosition -> BoundVariablePosition -> Bool Source # (<=) :: BoundVariablePosition -> BoundVariablePosition -> Bool Source # (>) :: BoundVariablePosition -> BoundVariablePosition -> Bool Source # (>=) :: BoundVariablePosition -> BoundVariablePosition -> Bool Source # max :: BoundVariablePosition -> BoundVariablePosition -> BoundVariablePosition Source # min :: BoundVariablePosition -> BoundVariablePosition -> BoundVariablePosition Source # | |
Constructors
| Inductive | |
| CoInductive |
Instances
| PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
| Pretty Induction Source # | |
| HasRange Induction Source # | |
| KillRange Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
| 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 | |