| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Common
Contents
- Delayed
- File
- Agda variants
- Record Directives
- Eta-equality
- Induction
- Hiding
- Modalities
- Quantities
- Relevance
- Annotations
- Locks
- Cohesion
- Origin of arguments (user-written, inserted or reflected)
- Free variable annotations
- Argument decoration
- Arguments
- Names
- Named arguments
- Range decoration.
- Raw names (before parsing into name parts).
- Further constructor and projection info
- Infixity, access, abstract, etc.
- NameId
- Meta variables
- Problems
- Placeholders (used to parse sections)
- Interaction meta variables
- Fixity
- Notation coupled with
Fixity - Import directive
- Termination
- Positivity
- Universe checking
- Universe checking
- Rewrite Directives on the LHS
- Information on expanded ellipsis (
...)
Description
Some common syntactic entities are defined in this module.
Synopsis
- type Nat = Int
- type Arity = Nat
- data Delayed
- data FileType
- data Cubical
- data Language
- data RecordDirectives' a = RecordDirectives {
- recInductive :: Maybe (Ranged Induction)
- recHasEta :: Maybe HasEta0
- recPattern :: Maybe Range
- recConstructor :: Maybe a
- emptyRecordDirectives :: RecordDirectives' a
- data HasEta' a
- type HasEta = HasEta' PatternOrCopattern
- type HasEta0 = HasEta' ()
- data PatternOrCopattern
- class PatternMatchingAllowed a where
- patternMatchingAllowed :: a -> Bool
- class CopatternMatchingAllowed a where
- copatternMatchingAllowed :: a -> Bool
- data Induction
- data Overlappable
- data Hiding
- data WithHiding a = WithHiding {}
- class LensHiding a where
- mergeHiding :: LensHiding a => WithHiding a -> a
- visible :: LensHiding a => a -> Bool
- notVisible :: LensHiding a => a -> Bool
- hidden :: LensHiding a => a -> Bool
- hide :: LensHiding a => a -> a
- hideOrKeepInstance :: LensHiding a => a -> a
- makeInstance :: LensHiding a => a -> a
- makeInstance' :: LensHiding a => Overlappable -> a -> a
- isOverlappable :: LensHiding a => a -> Bool
- isInstance :: LensHiding a => a -> Bool
- sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool
- newtype UnderAddition t = UnderAddition t
- newtype UnderComposition t = UnderComposition t
- data Modality = Modality {}
- moreUsableModality :: Modality -> Modality -> Bool
- usableModality :: LensModality a => a -> Bool
- composeModality :: Modality -> Modality -> Modality
- applyModality :: LensModality a => Modality -> a -> a
- inverseComposeModality :: Modality -> Modality -> Modality
- inverseApplyModalityButNotQuantity :: LensModality a => Modality -> a -> a
- addModality :: Modality -> Modality -> Modality
- zeroModality :: Modality
- unitModality :: Modality
- topModality :: Modality
- defaultModality :: Modality
- sameModality :: (LensModality a, LensModality b) => a -> b -> Bool
- lModRelevance :: Lens' Relevance Modality
- lModQuantity :: Lens' Quantity Modality
- lModCohesion :: Lens' Cohesion Modality
- class LensModality a where
- getModality :: a -> Modality
- setModality :: Modality -> a -> a
- mapModality :: (Modality -> Modality) -> a -> a
- getRelevanceMod :: LensModality a => LensGet Relevance a
- setRelevanceMod :: LensModality a => LensSet Relevance a
- mapRelevanceMod :: LensModality a => LensMap Relevance a
- getQuantityMod :: LensModality a => LensGet Quantity a
- setQuantityMod :: LensModality a => LensSet Quantity a
- mapQuantityMod :: LensModality a => LensMap Quantity a
- getCohesionMod :: LensModality a => LensGet Cohesion a
- setCohesionMod :: LensModality a => LensSet Cohesion a
- mapCohesionMod :: LensModality a => LensMap Cohesion a
- data Q0Origin
- = Q0Inferred
- | Q0 Range
- | Q0Erased Range
- data Q1Origin
- = Q1Inferred
- | Q1 Range
- | Q1Linear Range
- data QωOrigin
- = QωInferred
- | Qω Range
- | QωPlenty Range
- data Quantity
- sameQuantity :: Quantity -> Quantity -> Bool
- addQuantity :: Quantity -> Quantity -> Quantity
- zeroQuantity :: Quantity
- defaultQuantity :: Quantity
- unitQuantity :: Quantity
- topQuantity :: Quantity
- moreQuantity :: Quantity -> Quantity -> Bool
- composeQuantity :: Quantity -> Quantity -> Quantity
- applyQuantity :: LensQuantity a => Quantity -> a -> a
- inverseComposeQuantity :: Quantity -> Quantity -> Quantity
- inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a
- hasQuantity0 :: LensQuantity a => a -> Bool
- hasQuantity1 :: LensQuantity a => a -> Bool
- hasQuantityω :: LensQuantity a => a -> Bool
- noUserQuantity :: LensQuantity a => a -> Bool
- usableQuantity :: LensQuantity a => a -> Bool
- class LensQuantity a where
- getQuantity :: a -> Quantity
- setQuantity :: Quantity -> a -> a
- mapQuantity :: (Quantity -> Quantity) -> a -> a
- data Erased
- defaultErased :: Erased
- asQuantity :: Erased -> Quantity
- erasedFromQuantity :: Quantity -> Maybe Erased
- sameErased :: Erased -> Erased -> Bool
- isErased :: Erased -> Bool
- composeErased :: Erased -> Erased -> Erased
- data Relevance
- allRelevances :: [Relevance]
- class LensRelevance a where
- getRelevance :: a -> Relevance
- setRelevance :: Relevance -> a -> a
- mapRelevance :: (Relevance -> Relevance) -> a -> a
- isRelevant :: LensRelevance a => a -> Bool
- isIrrelevant :: LensRelevance a => a -> Bool
- isNonStrict :: LensRelevance a => a -> Bool
- moreRelevant :: Relevance -> Relevance -> Bool
- sameRelevance :: Relevance -> Relevance -> Bool
- usableRelevance :: LensRelevance a => a -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- applyRelevance :: LensRelevance a => Relevance -> a -> a
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a
- addRelevance :: Relevance -> Relevance -> Relevance
- zeroRelevance :: Relevance
- unitRelevance :: Relevance
- topRelevance :: Relevance
- defaultRelevance :: Relevance
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToRel :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- data Annotation = Annotation {}
- defaultAnnotation :: Annotation
- class LensAnnotation a where
- getAnnotation :: a -> Annotation
- setAnnotation :: Annotation -> a -> a
- mapAnnotation :: (Annotation -> Annotation) -> a -> a
- data Lock
- defaultLock :: Lock
- class LensLock a where
- data Cohesion
- = Flat
- | Continuous
- | Squash
- allCohesions :: [Cohesion]
- class LensCohesion a where
- getCohesion :: a -> Cohesion
- setCohesion :: Cohesion -> a -> a
- mapCohesion :: (Cohesion -> Cohesion) -> a -> a
- moreCohesion :: Cohesion -> Cohesion -> Bool
- sameCohesion :: Cohesion -> Cohesion -> Bool
- usableCohesion :: LensCohesion a => a -> Bool
- composeCohesion :: Cohesion -> Cohesion -> Cohesion
- applyCohesion :: LensCohesion a => Cohesion -> a -> a
- inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion
- inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a
- addCohesion :: Cohesion -> Cohesion -> Cohesion
- zeroCohesion :: Cohesion
- unitCohesion :: Cohesion
- topCohesion :: Cohesion
- defaultCohesion :: Cohesion
- data Origin
- data WithOrigin a = WithOrigin {}
- class LensOrigin a where
- 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
- data ArgInfo = ArgInfo {}
- class LensArgInfo a where
- getArgInfo :: a -> ArgInfo
- setArgInfo :: ArgInfo -> a -> a
- mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a
- defaultArgInfo :: ArgInfo
- getHidingArgInfo :: LensArgInfo a => LensGet Hiding a
- setHidingArgInfo :: LensArgInfo a => LensSet Hiding a
- mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a
- getModalityArgInfo :: LensArgInfo a => LensGet Modality a
- setModalityArgInfo :: LensArgInfo a => LensSet Modality a
- mapModalityArgInfo :: LensArgInfo a => LensMap Modality a
- getOriginArgInfo :: LensArgInfo a => LensGet Origin a
- setOriginArgInfo :: LensArgInfo a => LensSet Origin a
- mapOriginArgInfo :: LensArgInfo a => LensMap Origin a
- getFreeVariablesArgInfo :: LensArgInfo a => LensGet FreeVariables a
- setFreeVariablesArgInfo :: LensArgInfo a => LensSet FreeVariables a
- mapFreeVariablesArgInfo :: LensArgInfo a => LensMap FreeVariables a
- isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool
- data Arg e = Arg {}
- 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
- data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
- type Named_ = Named NamedName
- type NamedName = WithOrigin (Ranged ArgName)
- 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
- 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
- type NamedArg a = Arg (Named_ a)
- 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
- type ArgName = String
- argNameToString :: ArgName -> String
- stringToArgName :: String -> ArgName
- appendArgNames :: ArgName -> ArgName -> ArgName
- data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
- unranged :: a -> Ranged a
- type RawName = String
- rawNameToString :: RawName -> String
- stringToRawName :: String -> RawName
- type RString = Ranged RawName
- data ConOrigin
- bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin
- data ProjOrigin
- data IsInfix
- data Access
- data IsAbstract
- class LensIsAbstract a where
- class AnyIsAbstract a where
- anyIsAbstract :: a -> IsAbstract
- data IsInstance
- data IsMacro
- newtype ModuleNameHash = ModuleNameHash {}
- noModuleNameHash :: ModuleNameHash
- data NameId = NameId !Word64 !ModuleNameHash
- data MetaId = MetaId {
- metaId :: !Word64
- metaModule :: !ModuleNameHash
- newtype Constr a = Constr a
- newtype ProblemId = ProblemId Nat
- data PositionInName
- data MaybePlaceholder e
- noPlaceholder :: e -> MaybePlaceholder e
- newtype InteractionId = InteractionId {
- interactionId :: Nat
- type PrecedenceLevel = Double
- data FixityLevel
- data Associativity
- data Fixity = Fixity {}
- noFixity :: Fixity
- defaultFixity :: Fixity
- data Fixity' = Fixity' {
- theFixity :: !Fixity
- theNotation :: Notation
- theNameRange :: Range
- noFixity' :: Fixity'
- _fixityAssoc :: Lens' Associativity Fixity
- _fixityLevel :: Lens' FixityLevel Fixity
- class LensFixity a where
- lensFixity :: Lens' Fixity a
- class LensFixity' a where
- lensFixity' :: Lens' Fixity' a
- data ImportDirective' n m = ImportDirective {
- importDirRange :: Range
- using :: Using' n m
- hiding :: HidingDirective' n m
- impRenaming :: RenamingDirective' n m
- publicOpen :: Maybe Range
- type HidingDirective' n m = [ImportedName' n m]
- type RenamingDirective' n m = [Renaming' n m]
- defaultImportDir :: ImportDirective' n m
- isDefaultImportDir :: ImportDirective' n m -> Bool
- data Using' n m
- = UseEverything
- | Using [ImportedName' n m]
- mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2
- data ImportedName' n m
- = ImportedModule m
- | ImportedName n
- fromImportedName :: ImportedName' a a -> a
- setImportedName :: ImportedName' a a -> a -> ImportedName' a a
- partitionImportedNames :: [ImportedName' n m] -> ([n], [m])
- data Renaming' n m = Renaming {
- renFrom :: ImportedName' n m
- renTo :: ImportedName' n m
- renFixity :: Maybe Fixity
- renToRange :: Range
- data TerminationCheck m
- data PositivityCheck
- data UniverseCheck
- data CoverageCheck
- data RewriteEqn' qn nm p e
- data ExpandedEllipsis
- = ExpandedEllipsis { }
- | NoEllipsis
- type Notation = [NotationPart]
- noNotation :: Notation
- data BoundVariablePosition = BoundVariablePosition {
- holeNumber :: !Int
- varNumber :: !Int
- data NotationPart
Documentation
Delayed
Used to specify whether something should be delayed.
Constructors
| Delayed | |
| NotDelayed |
Instances
| KillRange Delayed Source # | |
Defined in Agda.Syntax.Common Methods | |
| EmbPrj Delayed Source # | |
| Generic Delayed Source # | |
Defined in Agda.Syntax.Common | |
| Show Delayed Source # | |
| NFData Delayed Source # | |
Defined in Agda.Syntax.Common | |
| Eq Delayed Source # | |
| Ord Delayed Source # | |
| type Rep Delayed Source # | |
File
Constructors
| AgdaFileType | |
| MdFileType | |
| RstFileType | |
| TexFileType | |
| OrgFileType |
Instances
| EmbPrj FileType Source # | |||||
| Pretty FileType Source # | |||||
| Generic FileType Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show FileType Source # | |||||
| NFData FileType Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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)))) | |||||
Agda variants
Variants of Cubical Agda.
Agda variants.
Only some variants are tracked.
Instances
Record Directives
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 # | |
| Functor RecordDirectives' Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> RecordDirectives' a -> RecordDirectives' b # (<$) :: a -> RecordDirectives' b -> RecordDirectives' a # | |
| 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 # | |
| Show a => Show (RecordDirectives' a) Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> RecordDirectives' a -> ShowS # show :: RecordDirectives' a -> String # showList :: [RecordDirectives' a] -> ShowS # | |
| NFData a => NFData (RecordDirectives' a) Source # | |
Defined in Agda.Syntax.Common Methods rnf :: RecordDirectives' a -> () # | |
| Eq a => Eq (RecordDirectives' a) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: RecordDirectives' a -> RecordDirectives' a -> Bool # (/=) :: RecordDirectives' a -> RecordDirectives' a -> Bool # | |
Eta-equality
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 # | |
| Foldable HasEta' Source # | |
Defined in Agda.Syntax.Common Methods fold :: Monoid m => HasEta' m -> m # foldMap :: Monoid m => (a -> m) -> HasEta' a -> m # foldMap' :: Monoid m => (a -> m) -> HasEta' a -> m # foldr :: (a -> b -> b) -> b -> HasEta' a -> b # foldr' :: (a -> b -> b) -> b -> HasEta' a -> b # foldl :: (b -> a -> b) -> b -> HasEta' a -> b # foldl' :: (b -> a -> b) -> b -> HasEta' a -> b # foldr1 :: (a -> a -> a) -> HasEta' a -> a # foldl1 :: (a -> a -> a) -> HasEta' a -> a # elem :: Eq a => a -> HasEta' a -> Bool # maximum :: Ord a => HasEta' a -> a # minimum :: Ord a => HasEta' a -> a # | |
| Traversable HasEta' Source # | |
| Functor HasEta' Source # | |
| 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 # | |
| Show a => Show (HasEta' a) Source # | |
| NFData a => NFData (HasEta' a) Source # | |
Defined in Agda.Syntax.Common | |
| Eq a => Eq (HasEta' a) Source # | |
| Ord a => Ord (HasEta' a) Source # | |
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 # | |
| 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 # | |
| HasRange PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods getRange :: PatternOrCopattern -> Range Source # | |
| KillRange PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods | |
| EmbPrj PatternOrCopattern Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| Bounded PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common | |
| Enum PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods succ :: PatternOrCopattern -> PatternOrCopattern # pred :: PatternOrCopattern -> PatternOrCopattern # toEnum :: Int -> PatternOrCopattern # fromEnum :: PatternOrCopattern -> Int # enumFrom :: PatternOrCopattern -> [PatternOrCopattern] # enumFromThen :: PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] # enumFromTo :: PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] # enumFromThenTo :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] # | |
| Show PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> PatternOrCopattern -> ShowS # show :: PatternOrCopattern -> String # showList :: [PatternOrCopattern] -> ShowS # | |
| NFData PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods rnf :: PatternOrCopattern -> () # | |
| Eq PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods (==) :: PatternOrCopattern -> PatternOrCopattern -> Bool # (/=) :: PatternOrCopattern -> PatternOrCopattern -> Bool # | |
| Ord PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods compare :: PatternOrCopattern -> PatternOrCopattern -> Ordering # (<) :: PatternOrCopattern -> PatternOrCopattern -> Bool # (<=) :: PatternOrCopattern -> PatternOrCopattern -> Bool # (>) :: PatternOrCopattern -> PatternOrCopattern -> Bool # (>=) :: PatternOrCopattern -> PatternOrCopattern -> Bool # max :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern # min :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern # | |
class PatternMatchingAllowed a where Source #
Can we pattern match on the record constructor?
Methods
patternMatchingAllowed :: a -> Bool Source #
Instances
| PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
| PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
| PatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
| 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 EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
Induction
Inductive < Coinductive
Constructors
| Inductive | |
| CoInductive |
Instances
| PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
| HasRange Induction Source # | |
| KillRange Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
| EmbPrj Induction Source # | |
| Pretty Induction Source # | |
| Show Induction Source # | |
| NFData Induction Source # | |
Defined in Agda.Syntax.Common | |
| Eq Induction Source # | |
| Ord Induction Source # | |
Hiding
data Overlappable Source #
Constructors
| YesOverlap | |
| NoOverlap |
Instances
| Monoid Overlappable Source # | |
Defined in Agda.Syntax.Common Methods mempty :: Overlappable # mappend :: Overlappable -> Overlappable -> Overlappable # mconcat :: [Overlappable] -> Overlappable # | |
| Semigroup Overlappable Source # | Just for the |
Defined in Agda.Syntax.Common Methods (<>) :: Overlappable -> Overlappable -> Overlappable # sconcat :: NonEmpty Overlappable -> Overlappable # stimes :: Integral b => b -> Overlappable -> Overlappable # | |
| Show Overlappable Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Overlappable -> ShowS # show :: Overlappable -> String # showList :: [Overlappable] -> ShowS # | |
| NFData Overlappable Source # | |
Defined in Agda.Syntax.Common Methods rnf :: Overlappable -> () # | |
| Eq Overlappable Source # | |
Defined in Agda.Syntax.Common | |
| Ord Overlappable Source # | |
Defined in Agda.Syntax.Common Methods compare :: Overlappable -> Overlappable -> Ordering # (<) :: Overlappable -> Overlappable -> Bool # (<=) :: Overlappable -> Overlappable -> Bool # (>) :: Overlappable -> Overlappable -> Bool # (>=) :: Overlappable -> Overlappable -> Bool # max :: Overlappable -> Overlappable -> Overlappable # min :: Overlappable -> Overlappable -> Overlappable # | |
Constructors
| Hidden | |
| Instance Overlappable | |
| NotHidden |
Instances
| LensHiding 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 # | |
| Pretty Hiding Source # | |
| Monoid Hiding Source # | |
| Semigroup Hiding Source # |
|
| Show Hiding Source # | |
| NFData Hiding Source # | |
Defined in Agda.Syntax.Common | |
| Eq Hiding Source # | |
| Ord Hiding Source # | |
| Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # | |
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 # | |||||
| Foldable WithHiding Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => WithHiding m -> m # foldMap :: Monoid m => (a -> m) -> WithHiding a -> m # foldMap' :: Monoid m => (a -> m) -> WithHiding a -> m # foldr :: (a -> b -> b) -> b -> WithHiding a -> b # foldr' :: (a -> b -> b) -> b -> WithHiding a -> b # foldl :: (b -> a -> b) -> b -> WithHiding a -> b # foldl' :: (b -> a -> b) -> b -> WithHiding a -> b # foldr1 :: (a -> a -> a) -> WithHiding a -> a # foldl1 :: (a -> a -> a) -> WithHiding a -> a # toList :: WithHiding a -> [a] # null :: WithHiding a -> Bool # length :: WithHiding a -> Int # elem :: Eq a => a -> WithHiding a -> Bool # maximum :: Ord a => WithHiding a -> a # minimum :: Ord a => WithHiding a -> a # sum :: Num a => WithHiding a -> a # product :: Num a => WithHiding a -> a # | |||||
| Traversable WithHiding Source # | |||||
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> WithHiding a -> f (WithHiding b) # sequenceA :: Applicative f => WithHiding (f a) -> f (WithHiding a) # mapM :: Monad m => (a -> m b) -> WithHiding a -> m (WithHiding b) # sequence :: Monad m => WithHiding (m a) -> m (WithHiding a) # | |||||
| Applicative WithHiding Source # | |||||
Defined in Agda.Syntax.Common Methods pure :: a -> WithHiding a # (<*>) :: WithHiding (a -> b) -> WithHiding a -> WithHiding b # liftA2 :: (a -> b -> c) -> WithHiding a -> WithHiding b -> WithHiding c # (*>) :: WithHiding a -> WithHiding b -> WithHiding b # (<*) :: WithHiding a -> WithHiding b -> WithHiding a # | |||||
| Functor WithHiding Source # | |||||
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> WithHiding a -> WithHiding b # (<$) :: a -> WithHiding b -> WithHiding a # | |||||
| 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 # | |||||
| 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 :: WithHiding a -> AbsToCon (ConOfAbs (WithHiding a)) Source # bindToConcrete :: WithHiding a -> (ConOfAbs (WithHiding a) -> AbsToCon b) -> AbsToCon b Source # | |||||
| ToAbstract c => ToAbstract (WithHiding c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract 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 # | |||||
| Pretty a => Pretty (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WithHiding a -> Doc Source # prettyPrec :: Int -> WithHiding a -> Doc Source # prettyList :: [WithHiding a] -> Doc Source # | |||||
| Show a => Show (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> WithHiding a -> ShowS # show :: WithHiding a -> String # showList :: [WithHiding a] -> ShowS # | |||||
| NFData a => NFData (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: WithHiding a -> () # | |||||
| Eq a => Eq (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Ord a => Ord (WithHiding a) Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: WithHiding a -> WithHiding a -> Ordering # (<) :: WithHiding a -> WithHiding a -> Bool # (<=) :: WithHiding a -> WithHiding a -> Bool # (>) :: WithHiding a -> WithHiding a -> Bool # (>=) :: WithHiding a -> WithHiding a -> Bool # max :: WithHiding a -> WithHiding a -> WithHiding a # min :: WithHiding a -> WithHiding a -> WithHiding a # | |||||
| AddContext (List1 (WithHiding Name), Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context 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 | |||||
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 (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 # | |
mergeHiding :: LensHiding a => WithHiding a -> a Source #
Monoidal composition of Hiding information in some data.
notVisible :: LensHiding a => a -> Bool Source #
:: LensHiding a => a -> Bool Source #
Hidden arguments are hidden.
hide :: LensHiding a => a -> a Source #
hideOrKeepInstance :: LensHiding a => a -> a Source #
makeInstance :: LensHiding a => a -> a Source #
makeInstance' :: LensHiding a => Overlappable -> a -> a Source #
isOverlappable :: LensHiding a => a -> Bool Source #
isInstance :: LensHiding a => a -> Bool Source #
sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool Source #
Ignores Overlappable.
Modalities
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 # (<*>) :: UnderAddition (a -> b) -> UnderAddition a -> UnderAddition b # liftA2 :: (a -> b -> c) -> UnderAddition a -> UnderAddition b -> UnderAddition c # (*>) :: UnderAddition a -> UnderAddition b -> UnderAddition b # (<*) :: UnderAddition a -> UnderAddition b -> UnderAddition a # | |
| Functor UnderAddition Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> UnderAddition a -> UnderAddition b # (<$) :: a -> UnderAddition b -> UnderAddition a # | |
| POMonoid (UnderAddition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
| POMonoid (UnderAddition Modality) Source # | |
Defined in Agda.Syntax.Common | |
| POMonoid (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
| POMonoid (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
| POSemigroup (UnderAddition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
| POSemigroup (UnderAddition Modality) Source # | |
Defined in Agda.Syntax.Common | |
| POSemigroup (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
| POSemigroup (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
| PartialOrd t => PartialOrd (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common Methods comparable :: Comparable (UnderAddition t) Source # | |
| Monoid (UnderAddition Cohesion) Source # |
|
Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Cohesion # mappend :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion # mconcat :: [UnderAddition Cohesion] -> UnderAddition Cohesion # | |
| Monoid (UnderAddition Modality) Source # | Pointwise additive unit. |
Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Modality # mappend :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality # mconcat :: [UnderAddition Modality] -> UnderAddition Modality # | |
| Monoid (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Quantity # mappend :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity # mconcat :: [UnderAddition Quantity] -> UnderAddition Quantity # | |
| Monoid (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Relevance # mappend :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance # mconcat :: [UnderAddition Relevance] -> UnderAddition Relevance # | |
| Semigroup (UnderAddition Cohesion) Source # |
|
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion # sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion # stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion # | |
| Semigroup (UnderAddition Modality) Source # | Pointwise addition. |
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality # sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality # stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality # | |
| Semigroup (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity # sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity # stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity # | |
| Semigroup (UnderAddition Relevance) Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance # sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance # stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance # | |
| Show t => Show (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> UnderAddition t -> ShowS # show :: UnderAddition t -> String # showList :: [UnderAddition t] -> ShowS # | |
| Eq t => Eq (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: UnderAddition t -> UnderAddition t -> Bool # (/=) :: UnderAddition t -> UnderAddition t -> Bool # | |
| Ord t => Ord (UnderAddition t) Source # | |
Defined in Agda.Syntax.Common Methods compare :: UnderAddition t -> UnderAddition t -> Ordering # (<) :: UnderAddition t -> UnderAddition t -> Bool # (<=) :: UnderAddition t -> UnderAddition t -> Bool # (>) :: UnderAddition t -> UnderAddition t -> Bool # (>=) :: UnderAddition t -> UnderAddition t -> Bool # max :: UnderAddition t -> UnderAddition t -> UnderAddition t # min :: UnderAddition t -> UnderAddition t -> UnderAddition t # | |
newtype UnderComposition t Source #
Type wrapper to indicate composition or multiplicative monoid/semigroup context.
Constructors
| UnderComposition t |
Instances
| Applicative UnderComposition Source # | |
Defined in Agda.Syntax.Common Methods pure :: a -> UnderComposition a # (<*>) :: UnderComposition (a -> b) -> UnderComposition a -> UnderComposition b # liftA2 :: (a -> b -> c) -> UnderComposition a -> UnderComposition b -> UnderComposition c # (*>) :: UnderComposition a -> UnderComposition b -> UnderComposition b # (<*) :: UnderComposition a -> UnderComposition b -> UnderComposition a # | |
| Functor UnderComposition Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> UnderComposition a -> UnderComposition b # (<$) :: a -> UnderComposition b -> UnderComposition a # | |
| 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 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 Quantity) Source # | |
Defined in Agda.Syntax.Common | |
| POMonoid (UnderComposition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
| POSemigroup (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
| POSemigroup (UnderComposition Modality) Source # | |
Defined in Agda.Syntax.Common | |
| POSemigroup (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
| POSemigroup (UnderComposition Relevance) Source # | |
Defined in Agda.Syntax.Common | |
| PartialOrd t => PartialOrd (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common Methods comparable :: Comparable (UnderComposition t) Source # | |
| Monoid (UnderComposition Cohesion) Source # |
|
Defined in Agda.Syntax.Common Methods mempty :: UnderComposition Cohesion # mappend :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion # mconcat :: [UnderComposition Cohesion] -> UnderComposition Cohesion # | |
| Monoid (UnderComposition Modality) Source # | Pointwise composition unit. |
Defined in Agda.Syntax.Common Methods mempty :: UnderComposition Modality # mappend :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality # mconcat :: [UnderComposition Modality] -> UnderComposition Modality # | |
| 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 Methods mempty :: UnderComposition Quantity # mappend :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity # mconcat :: [UnderComposition Quantity] -> UnderComposition Quantity # | |
| 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 # sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion # stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion # | |
| Semigroup (UnderComposition Erased) Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased # stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased # | |
| Semigroup (UnderComposition Modality) Source # | Pointwise composition. |
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality # sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality # stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality # | |
| Semigroup (UnderComposition Quantity) Source # | Composition of quantities (multiplication).
Right-biased for origin. |
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity # stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity # | |
| Semigroup (UnderComposition Relevance) Source # |
|
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance # sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance # stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance # | |
| Show t => Show (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> UnderComposition t -> ShowS # show :: UnderComposition t -> String # showList :: [UnderComposition t] -> ShowS # | |
| Eq t => Eq (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: UnderComposition t -> UnderComposition t -> Bool # (/=) :: UnderComposition t -> UnderComposition t -> Bool # | |
| Ord t => Ord (UnderComposition t) Source # | |
Defined in Agda.Syntax.Common Methods compare :: UnderComposition t -> UnderComposition t -> Ordering # (<) :: UnderComposition t -> UnderComposition t -> Bool # (<=) :: UnderComposition t -> UnderComposition t -> Bool # (>) :: UnderComposition t -> UnderComposition t -> Bool # (>=) :: UnderComposition t -> UnderComposition t -> Bool # max :: UnderComposition t -> UnderComposition t -> UnderComposition t # min :: UnderComposition t -> UnderComposition t -> UnderComposition t # | |
We have a tuple of modalities, which might not be fully orthogonal. For instance, irrelevant stuff is also run-time irrelevant.
Constructors
| Modality | |
Fields
| |
Instances
| LensCohesion Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| LensModality Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| LensQuantity Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| LensRelevance Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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 # | |||||
| PartialOrd Modality Source # | Dominance ordering. | ||||
Defined in Agda.Syntax.Common Methods | |||||
| Pretty Modality Source # | |||||
| Generic Modality Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Modality Source # | |||||
| NFData Modality Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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 # mappend :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality # mconcat :: [UnderAddition Modality] -> UnderAddition Modality # | |||||
| Monoid (UnderComposition Modality) Source # | Pointwise composition unit. | ||||
Defined in Agda.Syntax.Common Methods mempty :: UnderComposition Modality # mappend :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality # mconcat :: [UnderComposition Modality] -> UnderComposition Modality # | |||||
| Semigroup (UnderAddition Modality) Source # | Pointwise addition. | ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality # sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality # stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality # | |||||
| Semigroup (UnderComposition Modality) Source # | Pointwise composition. | ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality # sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality # stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality # | |||||
| type Rep Modality Source # | |||||
Defined in Agda.Syntax.Common type Rep Modality = D1 ('MetaData "Modality" "Agda.Syntax.Common" "Agda-2.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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)))) | |||||
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 #
composeModality :: Modality -> Modality -> Modality Source #
Multiplicative monoid (standard monoid).
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.
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).
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.
zeroModality :: Modality Source #
Identity under addition
unitModality :: Modality Source #
Identity under composition
topModality :: Modality 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 ω.
sameModality :: (LensModality a, LensModality b) => a -> b -> Bool Source #
Equality ignoring origin.
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 TCEnv Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| 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 | |
getRelevanceMod :: LensModality a => LensGet Relevance a Source #
setRelevanceMod :: LensModality a => LensSet Relevance a Source #
mapRelevanceMod :: LensModality a => LensMap Relevance a Source #
getQuantityMod :: LensModality a => LensGet Quantity a Source #
setQuantityMod :: LensModality a => LensSet Quantity a Source #
mapQuantityMod :: LensModality a => LensMap Quantity a Source #
getCohesionMod :: LensModality a => LensGet Cohesion a Source #
setCohesionMod :: LensModality a => LensSet Cohesion a Source #
mapCohesionMod :: LensModality a => LensMap Cohesion a Source #
Quantities
Quantity origin.
Origin of Quantity0.
Constructors
| Q0Inferred | User wrote nothing. |
| Q0 Range | User wrote "@0". |
| Q0Erased Range | User wrote "@erased". |
Instances
| HasRange Q0Origin Source # | |||||
| KillRange Q0Origin Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| SetRange Q0Origin Source # | |||||
| EmbPrj Q0Origin Source # | |||||
| Null Q0Origin Source # | |||||
| Pretty Q0Origin Source # | |||||
| 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 # | |||||
| NFData Q0Origin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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 Quantity1.
Constructors
| Q1Inferred | User wrote nothing. |
| Q1 Range | User wrote "@1". |
| Q1Linear Range | User wrote "@linear". |
Instances
| HasRange Q1Origin Source # | |||||
| KillRange Q1Origin Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| SetRange Q1Origin Source # | |||||
| EmbPrj Q1Origin Source # | |||||
| Null Q1Origin Source # | |||||
| Pretty Q1Origin Source # | |||||
| 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 # | |||||
| NFData Q1Origin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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)))) | |||||
Origin of Quantityω.
Constructors
| QωInferred | User wrote nothing. |
| Qω Range | User wrote "@ω". |
| QωPlenty Range | User wrote "@plenty". |
Instances
| 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 # | |||||
| Pretty QωOrigin Source # | |||||
| 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 # | |||||
| NFData QωOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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)))) | |||||
Instances for Q0Origin.
Instances for Q1Origin.
Instances for QωOrigin.
Quantity.
Quantity for linearity.
A quantity is a set of natural numbers, indicating possible semantic
uses of a variable. A singleton set {n} requires that the
corresponding variable is used exactly n times.
Constructors
| Quantity0 Q0Origin | Zero uses |
| Quantity1 Q1Origin | Linear use |
| Quantityω QωOrigin | Unrestricted use |
Instances
| LensQuantity Quantity Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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 # | |||||
| PartialOrd Quantity Source # | Note that the order is | ||||
Defined in Agda.Syntax.Common Methods | |||||
| Pretty Quantity Source # | |||||
| Generic Quantity Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Quantity Source # | |||||
| NFData Quantity Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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 # mappend :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity # mconcat :: [UnderAddition Quantity] -> UnderAddition Quantity # | |||||
| 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 Methods mempty :: UnderComposition Quantity # mappend :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity # mconcat :: [UnderComposition Quantity] -> UnderComposition Quantity # | |||||
| Semigroup (UnderAddition Quantity) Source # | |||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity # sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity # stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity # | |||||
| Semigroup (UnderComposition Quantity) Source # | Composition of quantities (multiplication).
Right-biased for origin. | ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity # stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity # | |||||
| type Rep Quantity Source # | |||||
Defined in Agda.Syntax.Common type Rep Quantity = D1 ('MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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)))) | |||||
addQuantity :: Quantity -> Quantity -> Quantity Source #
Quantity forms an additive monoid with zero Quantity0.
zeroQuantity :: Quantity Source #
Identity element under addition
defaultQuantity :: Quantity Source #
Absorptive element! This differs from Relevance and Cohesion whose default is the multiplicative unit.
unitQuantity :: Quantity Source #
Identity element under composition
topQuantity :: Quantity Source #
Absorptive element is ω.
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.
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).
inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a Source #
Left division by a Quantity.
Used e.g. to modify context when going into a q argument.
hasQuantity0 :: LensQuantity a => a -> Bool Source #
Check for Quantity0.
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?
usableQuantity :: LensQuantity a => a -> Bool Source #
A thing of quantity 0 is unusable, all others are usable.
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 TCEnv Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| 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 | |
Erased.
A special case of Quantity: erased or not.
Instances
| HasRange Erased Source # | |||||
| KillRange Erased Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| Generic Erased Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Erased Source # | |||||
| NFData Erased Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq Erased Source # | |||||
| Semigroup (UnderComposition Erased) Source # | |||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased # stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased # | |||||
| type Rep Erased Source # | |||||
Defined in Agda.Syntax.Common type Rep Erased = D1 ('MetaData "Erased" "Agda.Syntax.Common" "Agda-2.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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.
Relevance
A function argument can be relevant or irrelevant. See Agda.TypeChecking.Irrelevance.
Constructors
| Relevant | The argument is (possibly) relevant at compile-time. |
| NonStrict | The argument may never flow into evaluation position. Therefore, it is irrelevant at run-time. It is treated relevantly during equality checking. |
| Irrelevant | The argument is irrelevant at compile- and runtime. |
Instances
| LensRelevance Relevance Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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 # | |||||
| PartialOrd Relevance Source # | More relevant is smaller. | ||||
Defined in Agda.Syntax.Common Methods | |||||
| Pretty Relevance Source # | |||||
| Bounded Relevance Source # | |||||
| Enum Relevance Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: Relevance -> Relevance # pred :: Relevance -> Relevance # fromEnum :: Relevance -> Int # enumFrom :: Relevance -> [Relevance] # enumFromThen :: Relevance -> Relevance -> [Relevance] # enumFromTo :: Relevance -> Relevance -> [Relevance] # enumFromThenTo :: Relevance -> Relevance -> Relevance -> [Relevance] # | |||||
| Generic Relevance Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Relevance Source # | |||||
| NFData Relevance Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq Relevance Source # | |||||
| Ord Relevance Source # | More relevant is smaller. | ||||
| 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 # mappend :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance # mconcat :: [UnderAddition Relevance] -> UnderAddition Relevance # | |||||
| 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 # sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance # stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance # | |||||
| Semigroup (UnderComposition Relevance) Source # |
| ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance # sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance # stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance # | |||||
| type Rep Relevance Source # | |||||
Defined in Agda.Syntax.Common type Rep Relevance = D1 ('MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.6.3.1-LLs6QCSf11yD4oGFrJrY5P" 'False) (C1 ('MetaCons "Relevant" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonStrict" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Irrelevant" 'PrefixI 'False) (U1 :: Type -> Type))) | |||||
allRelevances :: [Relevance] Source #
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 TCEnv Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| LensRelevance (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
| LensRelevance (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
| LensRelevance (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal | |
| LensRelevance (FreeEnv' a b c) Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
isRelevant :: LensRelevance a => a -> Bool Source #
isIrrelevant :: LensRelevance a => a -> Bool Source #
isNonStrict :: LensRelevance a => a -> Bool Source #
moreRelevant :: Relevance -> Relevance -> Bool Source #
Information ordering.
Relevant `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
usableRelevance :: LensRelevance a => a -> Bool Source #
usableRelevance rel == False iff we cannot use a variable of rel.
composeRelevance :: Relevance -> Relevance -> Relevance Source #
Relevance composition.
Irrelevant is dominant, Relevant is neutral.
Composition coincides with max.
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.
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).
inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a Source #
Left division by a Relevance.
Used e.g. to modify context when going into a rel argument.
addRelevance :: Relevance -> Relevance -> Relevance Source #
Combine inferred Relevance.
The unit is Irrelevant.
zeroRelevance :: Relevance Source #
Relevance forms a monoid under addition, and even a semiring.
unitRelevance :: Relevance Source #
Identity element under composition
topRelevance :: Relevance Source #
Absorptive element under addition.
defaultRelevance :: Relevance Source #
Default Relevance is the identity element under composition
irrToNonStrict :: Relevance -> Relevance Source #
Irrelevant function arguments may appear non-strictly in the codomain type.
nonStrictToRel :: Relevance -> Relevance Source #
Applied when working on types (unless --experimental-irrelevance).
nonStrictToIrr :: Relevance -> Relevance Source #
Annotations
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 | |||||
| Generic Annotation Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Annotation Source # | |||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Annotation -> ShowS # show :: Annotation -> String # showList :: [Annotation] -> ShowS # | |||||
| NFData Annotation Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: Annotation -> () # | |||||
| Eq Annotation Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Ord Annotation Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: Annotation -> Annotation -> Ordering # (<) :: Annotation -> Annotation -> Bool # (<=) :: Annotation -> Annotation -> Bool # (>) :: Annotation -> Annotation -> Bool # (>=) :: Annotation -> Annotation -> Bool # max :: Annotation -> Annotation -> Annotation # min :: Annotation -> Annotation -> Annotation # | |||||
| type Rep Annotation Source # | |||||
Defined in Agda.Syntax.Common type Rep Annotation = D1 ('MetaData "Annotation" "Agda.Syntax.Common" "Agda-2.6.3.1-LLs6QCSf11yD4oGFrJrY5P" 'False) (C1 ('MetaCons "Annotation" 'PrefixI 'True) (S1 ('MetaSel ('Just "annLock") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lock))) | |||||
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 # | |
Locks
Constructors
| IsNotLock | |
| IsLock | In the future there might be different kinds of them. For now we assume lock weakening. |
Instances
defaultLock :: Lock Source #
class LensLock a where Source #
Minimal complete definition
Cohesion
Cohesion modalities see "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" (arXiv:1509.07584) types are now given an additional topological layer which the modalities interact with.
Constructors
| Flat | same points, discrete topology, idempotent comonad, box-like. |
| Continuous | identity modality. | Sharp -- ^ same points, codiscrete topology, idempotent monad, diamond-like. |
| Squash | single point space, artificially added for Flat left-composition. |
Instances
| LensCohesion Cohesion Source # | |||||
Defined in Agda.Syntax.Common | |||||
| HasRange Cohesion Source # | |||||
| KillRange Cohesion Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| SetRange Cohesion Source # | |||||
| Verbalize Cohesion Source # | |||||
| EmbPrj Cohesion Source # | |||||
| PartialOrd Cohesion Source # | Flatter is smaller. | ||||
Defined in Agda.Syntax.Common Methods | |||||
| Pretty Cohesion Source # | |||||
| Bounded Cohesion Source # | |||||
| Enum Cohesion Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic Cohesion Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show Cohesion Source # | |||||
| NFData Cohesion Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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 # mappend :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion # mconcat :: [UnderAddition Cohesion] -> UnderAddition Cohesion # | |||||
| Monoid (UnderComposition Cohesion) Source # |
| ||||
Defined in Agda.Syntax.Common Methods mempty :: UnderComposition Cohesion # mappend :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion # mconcat :: [UnderComposition Cohesion] -> UnderComposition Cohesion # | |||||
| Semigroup (UnderAddition Cohesion) Source # |
| ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion # sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion # stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion # | |||||
| Semigroup (UnderComposition Cohesion) Source # |
| ||||
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion # sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion # stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion # | |||||
| type Rep Cohesion Source # | |||||
Defined in Agda.Syntax.Common type Rep Cohesion = D1 ('MetaData "Cohesion" "Agda.Syntax.Common" "Agda-2.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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))) | |||||
allCohesions :: [Cohesion] Source #
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 (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
| LensCohesion (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal | |
moreCohesion :: Cohesion -> Cohesion -> Bool Source #
Information ordering.
Flat `moreCohesion`
Continuous `moreCohesion`
Sharp `moreCohesion`
Squash
usableCohesion :: LensCohesion a => a -> Bool Source #
usableCohesion rel == False iff we cannot use a variable of rel.
composeCohesion :: Cohesion -> Cohesion -> Cohesion Source #
Cohesion composition.
Squash is dominant, Continuous is neutral.
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.
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.
inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a Source #
Left division by a Cohesion.
Used e.g. to modify context when going into a rel argument.
zeroCohesion :: Cohesion Source #
Cohesion forms a monoid under addition, and even a semiring.
unitCohesion :: Cohesion Source #
Identity under composition
topCohesion :: Cohesion Source #
Absorptive element under addition.
defaultCohesion :: Cohesion Source #
Default Cohesion is the identity element under composition
Origin of arguments (user-written, inserted or reflected)
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" |
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 # | |
| Show Origin Source # | |
| NFData Origin Source # | |
Defined in Agda.Syntax.Common | |
| Eq Origin Source # | |
| Ord Origin Source # | |
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 # | |||||
| Foldable WithOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => WithOrigin m -> m # foldMap :: Monoid m => (a -> m) -> WithOrigin a -> m # foldMap' :: Monoid m => (a -> m) -> WithOrigin a -> m # foldr :: (a -> b -> b) -> b -> WithOrigin a -> b # foldr' :: (a -> b -> b) -> b -> WithOrigin a -> b # foldl :: (b -> a -> b) -> b -> WithOrigin a -> b # foldl' :: (b -> a -> b) -> b -> WithOrigin a -> b # foldr1 :: (a -> a -> a) -> WithOrigin a -> a # foldl1 :: (a -> a -> a) -> WithOrigin a -> a # toList :: WithOrigin a -> [a] # null :: WithOrigin a -> Bool # length :: WithOrigin a -> Int # elem :: Eq a => a -> WithOrigin a -> Bool # maximum :: Ord a => WithOrigin a -> a # minimum :: Ord a => WithOrigin a -> a # sum :: Num a => WithOrigin a -> a # product :: Num a => WithOrigin a -> a # | |||||
| Traversable WithOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> WithOrigin a -> f (WithOrigin b) # sequenceA :: Applicative f => WithOrigin (f a) -> f (WithOrigin a) # mapM :: Monad m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) # sequence :: Monad m => WithOrigin (m a) -> m (WithOrigin a) # | |||||
| Functor WithOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> WithOrigin a -> WithOrigin b # (<$) :: a -> WithOrigin b -> WithOrigin a # | |||||
| 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 # | |||||
| 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 # | |||||
| 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 # | |||||
| Show a => Show (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> WithOrigin a -> ShowS # show :: WithOrigin a -> String # showList :: [WithOrigin a] -> ShowS # | |||||
| NFData a => NFData (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: WithOrigin a -> () # | |||||
| Eq a => Eq (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Ord a => Ord (WithOrigin a) Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: WithOrigin a -> WithOrigin a -> Ordering # (<) :: WithOrigin a -> WithOrigin a -> Bool # (<=) :: WithOrigin a -> WithOrigin a -> Bool # (>) :: WithOrigin a -> WithOrigin a -> Bool # (>=) :: WithOrigin a -> WithOrigin a -> Bool # max :: WithOrigin a -> WithOrigin a -> WithOrigin a # min :: WithOrigin a -> WithOrigin a -> WithOrigin a # | |||||
| ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
| AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
| AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
| type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
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 (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 # | |
Free variable annotations
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 | |
| Monoid FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods mempty :: FreeVariables # mappend :: FreeVariables -> FreeVariables -> FreeVariables # mconcat :: [FreeVariables] -> FreeVariables # | |
| Semigroup FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: FreeVariables -> FreeVariables -> FreeVariables # sconcat :: NonEmpty FreeVariables -> FreeVariables # stimes :: Integral b => b -> FreeVariables -> FreeVariables # | |
| Show FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> FreeVariables -> ShowS # show :: FreeVariables -> String # showList :: [FreeVariables] -> ShowS # | |
| NFData FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods rnf :: FreeVariables -> () # | |
| Eq FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods (==) :: FreeVariables -> FreeVariables -> Bool # (/=) :: FreeVariables -> FreeVariables -> Bool # | |
| Ord FreeVariables Source # | |
Defined in Agda.Syntax.Common Methods compare :: FreeVariables -> FreeVariables -> Ordering # (<) :: FreeVariables -> FreeVariables -> Bool # (<=) :: FreeVariables -> FreeVariables -> Bool # (>) :: FreeVariables -> FreeVariables -> Bool # (>=) :: FreeVariables -> FreeVariables -> Bool # max :: FreeVariables -> FreeVariables -> FreeVariables # min :: FreeVariables -> FreeVariables -> FreeVariables # | |
oneFreeVariable :: Int -> FreeVariables Source #
freeVariablesFromList :: [Int] -> FreeVariables Source #
class LensFreeVariables a where Source #
A lens to access the FreeVariables attribute in data structures.
Minimal implementation: getFreeVariables and mapFreeVariables or LensArgInfo.
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 #
Argument decoration
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 # | |
| 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 # | |
| Show ArgInfo Source # | |
| NFData ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
| Eq ArgInfo Source # | |
| Ord ArgInfo Source # | |
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 (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 | |
getHidingArgInfo :: LensArgInfo a => LensGet Hiding a Source #
setHidingArgInfo :: LensArgInfo a => LensSet Hiding a Source #
mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a Source #
getModalityArgInfo :: LensArgInfo a => LensGet Modality a Source #
setModalityArgInfo :: LensArgInfo a => LensSet Modality a Source #
mapModalityArgInfo :: LensArgInfo a => LensMap Modality a Source #
getOriginArgInfo :: LensArgInfo a => LensGet Origin a Source #
setOriginArgInfo :: LensArgInfo a => LensSet Origin a Source #
mapOriginArgInfo :: LensArgInfo a => LensMap Origin a Source #
isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool Source #
Arguments
Instances
| MapNamedArgPattern NAP Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
| IsPrefixOf Args Source # | |||||
Defined in Agda.TypeChecking.Abstract | |||||
| Decoration Arg Source # | |||||
| Foldable Arg Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => Arg m -> m # foldMap :: Monoid m => (a -> m) -> Arg a -> m # foldMap' :: Monoid m => (a -> m) -> Arg a -> m # foldr :: (a -> b -> b) -> b -> Arg a -> b # foldr' :: (a -> b -> b) -> b -> Arg a -> b # foldl :: (b -> a -> b) -> b -> Arg a -> b # foldl' :: (b -> a -> b) -> b -> Arg a -> b # foldr1 :: (a -> a -> a) -> Arg a -> a # foldl1 :: (a -> a -> a) -> Arg a -> a # elem :: Eq a => a -> Arg a -> Bool # maximum :: Ord a => Arg a -> a # | |||||
| Traversable Arg Source # | |||||
| Functor Arg Source # | |||||
| Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # | |||||
| Conversion TOM Term (MExp O) Source # | |||||
| Conversion TOM Type (MExp O) Source # | |||||
| Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # | |||||
| MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
| PatternLike a b => PatternLike a (Arg b) Source # | |||||
| Conversion MOT (Exp O) Term Source # | |||||
| Conversion MOT (Exp O) Type Source # | |||||
| Conversion TOM (Arg Pattern) (Pat O) Source # | |||||
| Conversion TOM [Clause] [([Pat O], MExp O)] Source # | |||||
| Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # | |||||
| Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # | |||||
| SubstExpr a => SubstExpr (Arg a) Source # | |||||
| IsProjP a => IsProjP (Arg a) Source # | |||||
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |||||
| APatternLike a => APatternLike (Arg a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern Associated Types
| |||||
| DeclaredNames a => DeclaredNames (Arg a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Arg a -> m Source # | |||||
| ExprLike a => ExprLike (Arg a) Source # | |||||
Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Arg a) Source # foldExpr :: FoldExprFn m (Arg a) Source # traverseExpr :: TraverseExprFn m (Arg a) Source # | |||||
| LensAnnotation (Arg t) Source # | |||||
Defined in Agda.Syntax.Common Methods getAnnotation :: Arg t -> Annotation Source # setAnnotation :: Annotation -> Arg t -> Arg t Source # mapAnnotation :: (Annotation -> Annotation) -> Arg t -> Arg t Source # | |||||
| LensArgInfo (Arg a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| LensCohesion (Arg e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| LensFreeVariables (Arg e) Source # | |||||
Defined in Agda.Syntax.Common Methods getFreeVariables :: Arg e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Arg e -> Arg e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e Source # | |||||
| LensHiding (Arg e) Source # | |||||
| LensLock (Arg t) Source # | |||||
| LensModality (Arg e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| LensNamed a => LensNamed (Arg a) Source # | |||||
| LensOrigin (Arg e) Source # | |||||
| LensQuantity (Arg e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| LensRelevance (Arg e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| ExprLike a => ExprLike (Arg a) Source # | |||||
| CPatternLike p => CPatternLike (Arg p) Source # | |||||
Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Arg p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Arg p -> m (Arg p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Arg p -> m (Arg p) Source # | |||||
| IsWithP p => IsWithP (Arg p) Source # | |||||
| LensSort a => LensSort (Arg a) Source # | |||||
| PatternVars (Arg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
| PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
| GetDefs a => GetDefs (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Arg a -> m () Source # | |||||
| TermLike a => TermLike (Arg a) Source # | |||||
| AllMetas a => AllMetas (Arg a) Source # | |||||
| NamesIn a => NamesIn (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
| CountPatternVars a => CountPatternVars (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Arg a -> Int Source # | |||||
| PatternVarModalities a => PatternVarModalities (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern Associated Types
| |||||
| HasRange a => HasRange (Arg a) Source # | |||||
| KillRange a => KillRange (Arg a) Source # | |||||
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Arg a) Source # | |||||
| SetRange a => SetRange (Arg a) Source # | |||||
| ToConcrete a => ToConcrete (Arg a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
| |||||
| ToAbstract c => ToAbstract (Arg c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types
| |||||
| Reify i => Reify (Arg i) Source # | Skip reification of implicit and irrelevant args if option is off. | ||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
| ToAbstract r => ToAbstract (Arg r) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types
Methods toAbstract :: MonadReflectedToAbstract m => Arg r -> m (AbsOfRef (Arg r)) Source # | |||||
| ToAbstract r => ToAbstract [Arg r] Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types
Methods toAbstract :: MonadReflectedToAbstract m => [Arg r] -> m (AbsOfRef [Arg r]) Source # | |||||
| AbsTerm a => AbsTerm (Arg a) Source # | |||||
| EqualSy a => EqualSy (Arg a) Source # | Ignores irrelevant arguments and modality. (And, of course, origin and free variables). | ||||
| Free t => Free (Arg t) Source # | |||||
| PrecomputeFreeVars a => PrecomputeFreeVars (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Arg a -> FV (Arg a) Source # | |||||
| (Reduce a, ForceNotFree a) => ForceNotFree (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Arg a -> m (Arg a) | |||||
| UsableModality a => UsableModality (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Arg a -> m Bool Source # | |||||
| UsableRelevance a => UsableRelevance (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Arg a -> m Bool Source # | |||||
| NoProjectedVar a => NoProjectedVar (Arg a) Source # | |||||
Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Arg a -> Either ProjectedVar () Source # | |||||
| ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) Source # | |||||
Defined in Agda.TypeChecking.MetaVars | |||||
| MentionsMeta t => MentionsMeta (Arg t) Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
| AnyRigid a => AnyRigid (Arg a) Source # | |||||
| Occurs a => Occurs (Arg a) Source # | |||||
| IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Arg a -> m Bool Source # | |||||
| ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Abstract | |||||
| ComputeOccurrences a => ComputeOccurrences (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods occurrences :: Arg a -> OccM OccurrencesBuilder Source # | |||||
| PrettyTCM (Arg Expr) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| PrettyTCM (Arg Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| PrettyTCM (Arg Type) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| PrettyTCM (Arg Bool) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| PrettyTCM (NamedArg Expr) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| PrettyTCM (NamedArg Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| NormaliseProjP a => NormaliseProjP (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Arg a -> m (Arg a) Source # | |||||
| Instantiate t => Instantiate (Arg t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
| InstantiateFull t => InstantiateFull (Arg t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
| IsMeta a => IsMeta (Arg a) Source # | |||||
| Normalise t => Normalise (Arg t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
| Reduce t => Reduce (Arg t) Source # | |||||
| Simplify t => Simplify (Arg t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
| GetMatchables a => GetMatchables (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Arg a -> [QName] Source # | |||||
| IsFlexiblePattern a => IsFlexiblePattern (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Arg a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Arg a -> m Bool Source # | |||||
| EmbPrj a => EmbPrj (Arg a) Source # | |||||
| Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
| Subst a => Subst (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a Source # | |||||
| SynEq a => SynEq (Arg a) Source # | |||||
| PiApplyM a => PiApplyM (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Telescope Methods piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Arg a -> m Type Source # piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Arg a -> m Type Source # | |||||
| IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source # | |||||
| Unquote a => Unquote (Arg a) Source # | |||||
| Pretty a => Pretty (Arg a) Source # | |||||
| Show e => Show (Arg e) Source # | |||||
| NFData e => NFData (Arg e) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq e => Eq (Arg e) Source # | |||||
| Ord e => Ord (Arg e) Source # | |||||
| LabelPatVars a b => LabelPatVars (Arg a) (Arg b) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern Associated Types
Methods labelPatVars :: Arg a -> State [PatVarLabel (Arg b)] (Arg b) Source # unlabelPatVars :: Arg b -> Arg a Source # | |||||
| TermToPattern a b => TermToPattern (Arg a) (Arg b) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Internal | |||||
| ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
| ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
| NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
| Match t a b => Match (Dom t) (Arg a) (Arg b) Source # | |||||
| PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
| AddContext (List1 (Arg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
| AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
| AddContext ([Arg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # | |||||
| AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
| type ADotT (Arg a) Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
| type NameOf (Arg a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| type PatternVarOut (Arg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
| type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
| type PatVar (Arg a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
| type PatVarLabel (Arg b) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
| type ConOfAbs (Arg a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
| type AbsOfCon (Arg c) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
| type ReifiesTo (Arg i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
| type AbsOfRef (Arg r) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |||||
| type AbsOfRef [Arg r] Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |||||
| type SubstArg (Arg a) Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
defaultArg :: a -> Arg a Source #
withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] Source #
Names
class Eq a => Underscore a where Source #
Minimal complete definition
Instances
| Underscore Expr Source # | |
Defined in Agda.Syntax.Abstract | |
| 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 Doc Source # | |
Defined in Agda.Syntax.Common | |
| Underscore String Source # | |
Defined in Agda.Syntax.Common | |
Named arguments
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 # | |||||
| 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 # | |||||
| Pretty e => Pretty (Named_ e) Source # | |||||
| Foldable (Named name) Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => Named name m -> m # foldMap :: Monoid m => (a -> m) -> Named name a -> m # foldMap' :: Monoid m => (a -> m) -> Named name a -> m # foldr :: (a -> b -> b) -> b -> Named name a -> b # foldr' :: (a -> b -> b) -> b -> Named name a -> b # foldl :: (b -> a -> b) -> b -> Named name a -> b # foldl' :: (b -> a -> b) -> b -> Named name a -> b # foldr1 :: (a -> a -> a) -> Named name a -> a # foldl1 :: (a -> a -> a) -> Named name a -> a # toList :: Named name a -> [a] # null :: Named name a -> Bool # length :: Named name a -> Int # elem :: Eq a => a -> Named name a -> Bool # maximum :: Ord a => Named name a -> a # minimum :: Ord a => Named name a -> a # | |||||
| Traversable (Named name) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Functor (Named name) Source # | |||||
| ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
| SubstExpr a => SubstExpr (Named name a) Source # | |||||
| IsProjP a => IsProjP (Named n a) Source # | |||||
Defined in Agda.Syntax.Abstract.Name 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 # | |||||
| (Show name, Show a) => Show (Named name a) Source # | |||||
| (NFData name, NFData a) => NFData (Named name a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| (Eq name, Eq a) => Eq (Named name a) Source # | |||||
| (Ord name, Ord a) => Ord (Named name a) Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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 LensNamed a where Source #
Accessor/editor for the nameOf component.
Minimal complete definition
Nothing
Methods
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
ArgName
argNameToString :: ArgName -> String Source #
stringToArgName :: String -> ArgName Source #
Range decoration.
Thing with range info.
Constructors
| Ranged | |
Fields
| |
Instances
| MapNamedArgPattern NAP Source # | |||||
Defined in Agda.Syntax.Abstract.Pattern | |||||
| Decoration Ranged Source # | |||||
| Foldable Ranged Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => Ranged m -> m # foldMap :: Monoid m => (a -> m) -> Ranged a -> m # foldMap' :: Monoid m => (a -> m) -> Ranged a -> m # foldr :: (a -> b -> b) -> b -> Ranged a -> b # foldr' :: (a -> b -> b) -> b -> Ranged a -> b # foldl :: (b -> a -> b) -> b -> Ranged a -> b # foldl' :: (b -> a -> b) -> b -> Ranged a -> b # foldr1 :: (a -> a -> a) -> Ranged a -> a # foldl1 :: (a -> a -> a) -> Ranged a -> a # elem :: Eq a => a -> Ranged a -> Bool # maximum :: Ord a => Ranged a -> a # minimum :: Ord a => Ranged a -> a # | |||||
| Traversable Ranged Source # | |||||
| Functor Ranged Source # | |||||
| MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
| 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 # | |||||
| 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 (Ranged a) Source # | |||||
| Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
| DeBruijn a => DeBruijn (Named_ a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn | |||||
| IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source # | |||||
| Pretty e => Pretty (Named_ e) Source # | |||||
| Pretty a => Pretty (Ranged a) Source # | Ignores range. | ||||
| Show a => Show (Ranged a) Source # | |||||
| NFData a => NFData (Ranged a) Source # | Ranges are not forced. | ||||
Defined in Agda.Syntax.Common | |||||
| 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 | |||||
Raw names (before parsing into name parts).
rawNameToString :: RawName -> String Source #
stringToRawName :: String -> RawName Source #
Further constructor and projection info
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 # | |||||
| Bounded ConOrigin Source # | |||||
| Enum ConOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: ConOrigin -> ConOrigin # pred :: ConOrigin -> ConOrigin # fromEnum :: ConOrigin -> Int # enumFrom :: ConOrigin -> [ConOrigin] # enumFromThen :: ConOrigin -> ConOrigin -> [ConOrigin] # enumFromTo :: ConOrigin -> ConOrigin -> [ConOrigin] # enumFromThenTo :: ConOrigin -> ConOrigin -> ConOrigin -> [ConOrigin] # | |||||
| Generic ConOrigin Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show ConOrigin Source # | |||||
| NFData ConOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq ConOrigin Source # | |||||
| Ord ConOrigin Source # | |||||
| type Rep ConOrigin Source # | |||||
Defined in Agda.Syntax.Common type Rep ConOrigin = D1 ('MetaData "ConOrigin" "Agda.Syntax.Common" "Agda-2.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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))) | |||||
bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin Source #
Prefer user-written over system-inserted.
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 | |||||
| Bounded ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: ProjOrigin -> ProjOrigin # pred :: ProjOrigin -> ProjOrigin # toEnum :: Int -> ProjOrigin # fromEnum :: ProjOrigin -> Int # enumFrom :: ProjOrigin -> [ProjOrigin] # enumFromThen :: ProjOrigin -> ProjOrigin -> [ProjOrigin] # enumFromTo :: ProjOrigin -> ProjOrigin -> [ProjOrigin] # enumFromThenTo :: ProjOrigin -> ProjOrigin -> ProjOrigin -> [ProjOrigin] # | |||||
| Generic ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ProjOrigin -> ShowS # show :: ProjOrigin -> String # showList :: [ProjOrigin] -> ShowS # | |||||
| NFData ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: ProjOrigin -> () # | |||||
| Eq ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Ord ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: ProjOrigin -> ProjOrigin -> Ordering # (<) :: ProjOrigin -> ProjOrigin -> Bool # (<=) :: ProjOrigin -> ProjOrigin -> Bool # (>) :: ProjOrigin -> ProjOrigin -> Bool # (>=) :: ProjOrigin -> ProjOrigin -> Bool # max :: ProjOrigin -> ProjOrigin -> ProjOrigin # min :: ProjOrigin -> ProjOrigin -> ProjOrigin # | |||||
| type Rep ProjOrigin Source # | |||||
Defined in Agda.Syntax.Common type Rep ProjOrigin = D1 ('MetaData "ProjOrigin" "Agda.Syntax.Common" "Agda-2.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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))) | |||||
Infixity, access, abstract, etc.
Functions can be defined in both infix and prefix style. See
LHS.
private blocks, public imports
Access modifier.
Constructors
| PrivateAccess Origin | Store the |
| PublicAccess |
abstract blocks
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 | |||||
| Monoid IsAbstract Source # | Default is | ||||
Defined in Agda.Syntax.Common Methods mempty :: IsAbstract # mappend :: IsAbstract -> IsAbstract -> IsAbstract # mconcat :: [IsAbstract] -> IsAbstract # | |||||
| Semigroup IsAbstract Source # | Semigroup computes if any of several is an | ||||
Defined in Agda.Syntax.Common Methods (<>) :: IsAbstract -> IsAbstract -> IsAbstract # sconcat :: NonEmpty IsAbstract -> IsAbstract # stimes :: Integral b => b -> IsAbstract -> IsAbstract # | |||||
| Generic IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsAbstract -> ShowS # show :: IsAbstract -> String # showList :: [IsAbstract] -> ShowS # | |||||
| NFData IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: IsAbstract -> () # | |||||
| Eq IsAbstract Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Ord IsAbstract Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: IsAbstract -> IsAbstract -> Ordering # (<) :: IsAbstract -> IsAbstract -> Bool # (<=) :: IsAbstract -> IsAbstract -> Bool # (>) :: IsAbstract -> IsAbstract -> Bool # (>=) :: IsAbstract -> IsAbstract -> Bool # max :: IsAbstract -> IsAbstract -> IsAbstract # min :: IsAbstract -> IsAbstract -> IsAbstract # | |||||
| type Rep IsAbstract Source # | |||||
class LensIsAbstract a where Source #
Methods
lensIsAbstract :: Lens' IsAbstract a 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' IsAbstract (DefInfo' t) Source # | |
| LensIsAbstract (Closure a) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods lensIsAbstract :: Lens' IsAbstract (Closure a) 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 # | |
instance blocks
data IsInstance Source #
Is this definition eligible for instance search?
Constructors
| InstanceDef Range | 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 | |
| Show IsInstance Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsInstance -> ShowS # show :: IsInstance -> String # showList :: [IsInstance] -> ShowS # | |
| NFData IsInstance Source # | |
Defined in Agda.Syntax.Common Methods rnf :: IsInstance -> () # | |
| Eq IsInstance Source # | |
Defined in Agda.Syntax.Common | |
| Ord IsInstance Source # | |
Defined in Agda.Syntax.Common Methods compare :: IsInstance -> IsInstance -> Ordering # (<) :: IsInstance -> IsInstance -> Bool # (<=) :: IsInstance -> IsInstance -> Bool # (>) :: IsInstance -> IsInstance -> Bool # (>=) :: IsInstance -> IsInstance -> Bool # max :: IsInstance -> IsInstance -> IsInstance # min :: IsInstance -> IsInstance -> IsInstance # | |
macro blocks
Is this a macro definition?
Constructors
| MacroDef | |
| NotMacroDef |
Instances
| HasRange IsMacro Source # | |
| KillRange IsMacro Source # | |
Defined in Agda.Syntax.Common Methods | |
| Generic IsMacro Source # | |
Defined in Agda.Syntax.Common | |
| Show IsMacro Source # | |
| NFData IsMacro Source # | |
Defined in Agda.Syntax.Common | |
| Eq IsMacro Source # | |
| Ord IsMacro Source # | |
| type Rep IsMacro Source # | |
NameId
newtype ModuleNameHash Source #
Constructors
| ModuleNameHash | |
Fields | |
Instances
| EmbPrj ModuleNameHash Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Common | |||||
| HasTag ModuleNameHash Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods tag :: ModuleNameHash -> Maybe (Tag ModuleNameHash) Source # | |||||
| ToJSON ModuleNameHash Source # | |||||
Defined in Agda.Interaction.JSONTop Methods toJSON :: ModuleNameHash -> Value # toEncoding :: ModuleNameHash -> Encoding # toJSONList :: [ModuleNameHash] -> Value # toEncodingList :: [ModuleNameHash] -> Encoding # omitField :: ModuleNameHash -> Bool # | |||||
| Show ModuleNameHash Source # | The record selector is not included in the resulting strings. | ||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ModuleNameHash -> ShowS # show :: ModuleNameHash -> String # showList :: [ModuleNameHash] -> ShowS # | |||||
| NFData ModuleNameHash Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: ModuleNameHash -> () # | |||||
| Eq ModuleNameHash Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: ModuleNameHash -> ModuleNameHash -> Bool # (/=) :: ModuleNameHash -> ModuleNameHash -> Bool # | |||||
| Ord ModuleNameHash Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: ModuleNameHash -> ModuleNameHash -> Ordering # (<) :: ModuleNameHash -> ModuleNameHash -> Bool # (<=) :: ModuleNameHash -> ModuleNameHash -> Bool # (>) :: ModuleNameHash -> ModuleNameHash -> Bool # (>=) :: ModuleNameHash -> ModuleNameHash -> Bool # max :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash # min :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash # | |||||
| Hashable ModuleNameHash Source # | |||||
Defined in Agda.Syntax.Common | |||||
| NFData (BiMap RawTopLevelModuleName ModuleNameHash) Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: BiMap RawTopLevelModuleName ModuleNameHash -> () # | |||||
| type Tag ModuleNameHash Source # | |||||
Defined in Agda.Syntax.Common | |||||
The unique identifier of a name. Second argument is the top-level module identifier.
Constructors
| NameId !Word64 !ModuleNameHash |
Instances
| KillRange NameId Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| HasFresh NameId Source # | |||||
| EmbPrj NameId Source # | |||||
| Pretty NameId Source # | |||||
| Enum NameId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic NameId Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show NameId Source # | |||||
| NFData NameId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Eq NameId Source # | |||||
| Ord NameId Source # | |||||
| Hashable NameId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| MonadFresh NameId AbsToCon Source # | |||||
| 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.6.3.1-LLs6QCSf11yD4oGFrJrY5P" '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))) | |||||
Meta variables
Meta-variable identifiers use the same structure as NameIds.
Constructors
| MetaId | |
Fields
| |
Instances
| EncodeTCM 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 :: (MonadFail m, 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 # | |||||
| Pretty MetaId Source # | |||||
| ToJSON MetaId Source # | |||||
| Enum MetaId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Generic MetaId Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show MetaId Source # | The record selectors are not included in the resulting strings. | ||||
| NFData MetaId Source # | |||||
Defined in Agda.Syntax.Common | |||||
| 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.6.3.1-LLs6QCSf11yD4oGFrJrY5P" 'False) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Just "metaModule") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash))) | |||||
Constructors
| Constr a |
Instances
| ToConcrete (Constr Constructor) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor)) Source # bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon b Source # | |||||
| type ConOfAbs (Constr Constructor) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
Problems
A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.
Instances
| EncodeTCM ProblemId Source # | |
| HasFresh ProblemId Source # | |
| PrettyTCM ProblemId Source # | |
Defined in Agda.TypeChecking.Pretty | |
| Pretty ProblemId Source # | |
| ToJSON ProblemId Source # | |
| Enum ProblemId Source # | |
Defined in Agda.Syntax.Common Methods succ :: ProblemId -> ProblemId # pred :: ProblemId -> ProblemId # fromEnum :: ProblemId -> Int # enumFrom :: ProblemId -> [ProblemId] # enumFromThen :: ProblemId -> ProblemId -> [ProblemId] # enumFromTo :: ProblemId -> ProblemId -> [ProblemId] # enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId] # | |
| Num ProblemId Source # | |
Defined in Agda.Syntax.Common | |
| Integral ProblemId Source # | |
Defined in Agda.Syntax.Common Methods quot :: ProblemId -> ProblemId -> ProblemId # rem :: ProblemId -> ProblemId -> ProblemId # div :: ProblemId -> ProblemId -> ProblemId # mod :: ProblemId -> ProblemId -> ProblemId # quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId) # divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId) # | |
| Real ProblemId Source # | |
Defined in Agda.Syntax.Common Methods toRational :: ProblemId -> Rational # | |
| Show ProblemId Source # | |
| NFData ProblemId Source # | |
Defined in Agda.Syntax.Common | |
| Eq ProblemId Source # | |
| Ord ProblemId Source # | |
| Monad m => MonadFresh ProblemId (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m ProblemId Source # | |
Placeholders (used to parse sections)
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 Methods showsPrec :: Int -> PositionInName -> ShowS # show :: PositionInName -> String # showList :: [PositionInName] -> ShowS # | |
| Eq PositionInName Source # | |
Defined in Agda.Syntax.Common Methods (==) :: PositionInName -> PositionInName -> Bool # (/=) :: PositionInName -> PositionInName -> Bool # | |
| Ord PositionInName Source # | |
Defined in Agda.Syntax.Common Methods compare :: PositionInName -> PositionInName -> Ordering # (<) :: PositionInName -> PositionInName -> Bool # (<=) :: PositionInName -> PositionInName -> Bool # (>) :: PositionInName -> PositionInName -> Bool # (>=) :: PositionInName -> PositionInName -> Bool # max :: PositionInName -> PositionInName -> PositionInName # min :: PositionInName -> PositionInName -> PositionInName # | |
data MaybePlaceholder e Source #
Placeholders are used to represent the underscores in a section.
Constructors
| Placeholder !PositionInName | |
| NoPlaceholder !(Maybe PositionInName) e | The second argument is used only (but not always) for name parts other than underscores. |
Instances
| Foldable MaybePlaceholder Source # | |
Defined in Agda.Syntax.Common Methods fold :: Monoid m => MaybePlaceholder m -> m # foldMap :: Monoid m => (a -> m) -> MaybePlaceholder a -> m # foldMap' :: Monoid m => (a -> m) -> MaybePlaceholder a -> m # foldr :: (a -> b -> b) -> b -> MaybePlaceholder a -> b # foldr' :: (a -> b -> b) -> b -> MaybePlaceholder a -> b # foldl :: (b -> a -> b) -> b -> MaybePlaceholder a -> b # foldl' :: (b -> a -> b) -> b -> MaybePlaceholder a -> b # foldr1 :: (a -> a -> a) -> MaybePlaceholder a -> a # foldl1 :: (a -> a -> a) -> MaybePlaceholder a -> a # toList :: MaybePlaceholder a -> [a] # null :: MaybePlaceholder a -> Bool # length :: MaybePlaceholder a -> Int # elem :: Eq a => a -> MaybePlaceholder a -> Bool # maximum :: Ord a => MaybePlaceholder a -> a # minimum :: Ord a => MaybePlaceholder a -> a # sum :: Num a => MaybePlaceholder a -> a # product :: Num a => MaybePlaceholder a -> a # | |
| Traversable MaybePlaceholder Source # | |
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> MaybePlaceholder a -> f (MaybePlaceholder b) # sequenceA :: Applicative f => MaybePlaceholder (f a) -> f (MaybePlaceholder a) # mapM :: Monad m => (a -> m b) -> MaybePlaceholder a -> m (MaybePlaceholder b) # sequence :: Monad m => MaybePlaceholder (m a) -> m (MaybePlaceholder a) # | |
| Functor MaybePlaceholder Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b # (<$) :: a -> MaybePlaceholder b -> MaybePlaceholder a # | |
| 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 # | |
| 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 # | |
| Show e => Show (MaybePlaceholder e) Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> MaybePlaceholder e -> ShowS # show :: MaybePlaceholder e -> String # showList :: [MaybePlaceholder e] -> ShowS # | |
| NFData a => NFData (MaybePlaceholder a) Source # | |
Defined in Agda.Syntax.Common Methods rnf :: MaybePlaceholder a -> () # | |
| Eq e => Eq (MaybePlaceholder e) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (/=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # | |
| Ord e => Ord (MaybePlaceholder e) Source # | |
Defined in Agda.Syntax.Common Methods compare :: MaybePlaceholder e -> MaybePlaceholder e -> Ordering # (<) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (<=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (>) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (>=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # max :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e # min :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e # | |
noPlaceholder :: e -> MaybePlaceholder e Source #
An abbreviation: noPlaceholder = .NoPlaceholder
Nothing
Interaction meta variables
newtype InteractionId Source #
Constructors
| InteractionId | |
Fields
| |
Instances
| EncodeTCM InteractionId Source # | |||||
Defined in Agda.Interaction.JSONTop | |||||
| KillRange InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| ToConcrete InteractionId Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: InteractionId -> AbsToCon (ConOfAbs InteractionId) Source # bindToConcrete :: InteractionId -> (ConOfAbs InteractionId -> AbsToCon b) -> AbsToCon b Source # | |||||
| HasFresh InteractionId Source # | |||||
Defined in Agda.TypeChecking.Monad.Base | |||||
| Pretty InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods pretty :: InteractionId -> Doc Source # prettyPrec :: Int -> InteractionId -> Doc Source # prettyList :: [InteractionId] -> Doc Source # | |||||
| ToJSON InteractionId Source # | |||||
Defined in Agda.Interaction.JSONTop Methods toJSON :: InteractionId -> Value # toEncoding :: InteractionId -> Encoding # toJSONList :: [InteractionId] -> Value # toEncodingList :: [InteractionId] -> Encoding # omitField :: InteractionId -> Bool # | |||||
| Enum InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: InteractionId -> InteractionId # pred :: InteractionId -> InteractionId # toEnum :: Int -> InteractionId # fromEnum :: InteractionId -> Int # enumFrom :: InteractionId -> [InteractionId] # enumFromThen :: InteractionId -> InteractionId -> [InteractionId] # enumFromTo :: InteractionId -> InteractionId -> [InteractionId] # enumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId] # | |||||
| Num InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods (+) :: InteractionId -> InteractionId -> InteractionId # (-) :: InteractionId -> InteractionId -> InteractionId # (*) :: InteractionId -> InteractionId -> InteractionId # negate :: InteractionId -> InteractionId # abs :: InteractionId -> InteractionId # signum :: InteractionId -> InteractionId # fromInteger :: Integer -> InteractionId # | |||||
| Read InteractionId Source # | |||||
Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS InteractionId # readList :: ReadS [InteractionId] # | |||||
| Integral InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods quot :: InteractionId -> InteractionId -> InteractionId # rem :: InteractionId -> InteractionId -> InteractionId # div :: InteractionId -> InteractionId -> InteractionId # mod :: InteractionId -> InteractionId -> InteractionId # quotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId) # divMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId) # toInteger :: InteractionId -> Integer # | |||||
| Real InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods toRational :: InteractionId -> Rational # | |||||
| Show InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> InteractionId -> ShowS # show :: InteractionId -> String # showList :: [InteractionId] -> ShowS # | |||||
| NFData InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: InteractionId -> () # | |||||
| NFData InteractionPoints Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: InteractionPoints -> () # | |||||
| Eq InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: InteractionId -> InteractionId -> Bool # (/=) :: InteractionId -> InteractionId -> Bool # | |||||
| Ord InteractionId Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: InteractionId -> InteractionId -> Ordering # (<) :: InteractionId -> InteractionId -> Bool # (<=) :: InteractionId -> InteractionId -> Bool # (>) :: InteractionId -> InteractionId -> Bool # (>=) :: InteractionId -> InteractionId -> Bool # max :: InteractionId -> InteractionId -> InteractionId # min :: InteractionId -> InteractionId -> InteractionId # | |||||
| type ConOfAbs InteractionId Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
Fixity
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
| 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 | |
| Pretty FixityLevel Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: FixityLevel -> Doc Source # prettyPrec :: Int -> FixityLevel -> Doc Source # prettyList :: [FixityLevel] -> Doc Source # | |
| Show FixityLevel Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> FixityLevel -> ShowS # show :: FixityLevel -> String # showList :: [FixityLevel] -> ShowS # | |
| NFData FixityLevel Source # | |
Defined in Agda.Syntax.Common Methods rnf :: FixityLevel -> () # | |
| Eq FixityLevel Source # | |
Defined in Agda.Syntax.Common | |
| Ord FixityLevel Source # | |
Defined in Agda.Syntax.Common Methods compare :: FixityLevel -> FixityLevel -> Ordering # (<) :: FixityLevel -> FixityLevel -> Bool # (<=) :: FixityLevel -> FixityLevel -> Bool # (>) :: FixityLevel -> FixityLevel -> Bool # (>=) :: FixityLevel -> FixityLevel -> Bool # max :: FixityLevel -> FixityLevel -> FixityLevel # min :: FixityLevel -> FixityLevel -> FixityLevel # | |
data Associativity Source #
Associativity.
Constructors
| NonAssoc | |
| LeftAssoc | |
| RightAssoc |
Instances
| ToTerm Associativity Source # | |
Defined in Agda.TypeChecking.Primitive | |
| EmbPrj Associativity Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| Pretty Associativity Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Associativity -> Doc Source # prettyPrec :: Int -> Associativity -> Doc Source # prettyList :: [Associativity] -> Doc Source # | |
| Show Associativity Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Associativity -> ShowS # show :: Associativity -> String # showList :: [Associativity] -> ShowS # | |
| Eq Associativity Source # | |
Defined in Agda.Syntax.Common Methods (==) :: Associativity -> Associativity -> Bool # (/=) :: Associativity -> Associativity -> Bool # | |
| Ord Associativity Source # | |
Defined in Agda.Syntax.Common Methods compare :: Associativity -> Associativity -> Ordering # (<) :: Associativity -> Associativity -> Bool # (<=) :: Associativity -> Associativity -> Bool # (>) :: Associativity -> Associativity -> Bool # (>=) :: Associativity -> Associativity -> Bool # max :: Associativity -> Associativity -> Associativity # min :: Associativity -> Associativity -> Associativity # | |
Fixity of operators.
Constructors
| Fixity | |
Fields
| |
Instances
| LensFixity Fixity Source # | |
Defined in Agda.Syntax.Common | |
| HasRange Fixity Source # | |
| KillRange Fixity Source # | |
Defined in Agda.Syntax.Common Methods | |
| ToTerm Fixity Source # | |
| EmbPrj Fixity Source # | |
| Null Fixity Source # | |
| Pretty Fixity Source # | |
| Show Fixity Source # | |
| NFData Fixity Source # | |
Defined in Agda.Syntax.Common | |
| Eq Fixity Source # | |
| Ord Fixity Source # | |
Notation coupled with Fixity
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 | |
| KillRange Fixity' Source # | |
Defined in Agda.Syntax.Common Methods | |
| PrimTerm Fixity' Source # | |
| PrimType Fixity' Source # | |
| ToTerm Fixity' Source # | |
| EmbPrj Fixity' Source # | |
| Null Fixity' Source # | |
| Pretty Fixity' Source # | |
| Show Fixity' Source # | |
| NFData Fixity' Source # | |
Defined in Agda.Syntax.Common | |
| Eq Fixity' Source # | |
class LensFixity a where Source #
Methods
lensFixity :: Lens' Fixity a 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' Fixity (ThingWithFixity a) Source # | |
class LensFixity' a where Source #
Methods
lensFixity' :: Lens' Fixity' a 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' Fixity' (ThingWithFixity a) Source # | |
Import directive
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
| (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 | |
| (Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ImportDirective' a b -> Doc Source # prettyPrec :: Int -> ImportDirective' a b -> Doc Source # prettyList :: [ImportDirective' a b] -> Doc Source # | |
| (HasRange n, HasRange m) => Monoid (ImportDirective' n m) Source # | |
Defined in Agda.Syntax.Common Methods mempty :: ImportDirective' n m # mappend :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m # mconcat :: [ImportDirective' n m] -> ImportDirective' n m # | |
| (HasRange n, HasRange m) => Semigroup (ImportDirective' n m) Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m # sconcat :: NonEmpty (ImportDirective' n m) -> ImportDirective' n m # stimes :: Integral b => b -> ImportDirective' n m -> ImportDirective' n m # | |
| (Show a, Show b) => Show (ImportDirective' a b) Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ImportDirective' a b -> ShowS # show :: ImportDirective' a b -> String # showList :: [ImportDirective' a b] -> ShowS # | |
| (NFData a, NFData b) => NFData (ImportDirective' a b) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common Methods rnf :: ImportDirective' a b -> () # | |
| (Eq m, Eq n) => Eq (ImportDirective' n m) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: ImportDirective' n m -> ImportDirective' n m -> Bool # (/=) :: ImportDirective' n m -> ImportDirective' n m -> Bool # | |
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.
The using clause of import directive.
Constructors
| UseEverything | No |
| Using [ImportedName' n m] |
|
Instances
| (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 # | |
| (Pretty a, Pretty b) => Pretty (Using' a b) Source # | |
| Monoid (Using' n m) Source # | |
| Semigroup (Using' n m) Source # | |
| (Show a, Show b) => Show (Using' a b) Source # | |
| (NFData a, NFData b) => NFData (Using' a b) Source # | |
Defined in Agda.Syntax.Common | |
| (Eq m, Eq n) => Eq (Using' n m) Source # | |
mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2 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
| (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 | |
| (Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ImportedName' a b -> Doc Source # prettyPrec :: Int -> ImportedName' a b -> Doc Source # prettyList :: [ImportedName' a b] -> Doc Source # | |
| (Show m, Show n) => Show (ImportedName' n m) Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ImportedName' n m -> ShowS # show :: ImportedName' n m -> String # showList :: [ImportedName' n m] -> ShowS # | |
| (NFData a, NFData b) => NFData (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common Methods rnf :: ImportedName' a b -> () # | |
| (Eq m, Eq n) => Eq (ImportedName' n m) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: ImportedName' n m -> ImportedName' n m -> Bool # (/=) :: ImportedName' n m -> ImportedName' n m -> Bool # | |
| (Ord m, Ord n) => Ord (ImportedName' n m) Source # | |
Defined in Agda.Syntax.Common Methods compare :: ImportedName' n m -> ImportedName' n m -> Ordering # (<) :: ImportedName' n m -> ImportedName' n m -> Bool # (<=) :: ImportedName' n m -> ImportedName' n m -> Bool # (>) :: ImportedName' n m -> ImportedName' n m -> Bool # (>=) :: ImportedName' n m -> ImportedName' n m -> Bool # max :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m # min :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m # | |
fromImportedName :: ImportedName' a a -> a Source #
setImportedName :: ImportedName' a a -> a -> ImportedName' a a Source #
partitionImportedNames :: [ImportedName' n m] -> ([n], [m]) Source #
Like partitionEithers.
Constructors
| Renaming | |
Fields
| |
Instances
| (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 # | |
| (Pretty a, Pretty b) => Pretty (Renaming' a b) Source # | |
| (Show a, Show b) => Show (Renaming' a b) Source # | |
| (NFData a, NFData b) => NFData (Renaming' a b) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common | |
| (Eq m, Eq n) => Eq (Renaming' n m) Source # | |
HasRange instances
KillRange instances
NFData instances
Termination
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 # (<$) :: a -> TerminationCheck b -> TerminationCheck a # | |
| KillRange m => KillRange (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (TerminationCheck m) Source # | |
| Show m => Show (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> TerminationCheck m -> ShowS # show :: TerminationCheck m -> String # showList :: [TerminationCheck m] -> ShowS # | |
| NFData a => NFData (TerminationCheck a) Source # | |
Defined in Agda.Syntax.Common Methods rnf :: TerminationCheck a -> () # | |
| Eq m => Eq (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: TerminationCheck m -> TerminationCheck m -> Bool # (/=) :: TerminationCheck m -> TerminationCheck m -> Bool # | |
Positivity
data PositivityCheck Source #
Positivity check? (Default = True).
Constructors
| YesPositivityCheck | |
| NoPositivityCheck |
Instances
| KillRange PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| Monoid PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods mappend :: PositivityCheck -> PositivityCheck -> PositivityCheck # mconcat :: [PositivityCheck] -> PositivityCheck # | |||||
| Semigroup PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods (<>) :: PositivityCheck -> PositivityCheck -> PositivityCheck # sconcat :: NonEmpty PositivityCheck -> PositivityCheck # stimes :: Integral b => b -> PositivityCheck -> PositivityCheck # | |||||
| Bounded PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: PositivityCheck -> PositivityCheck # pred :: PositivityCheck -> PositivityCheck # toEnum :: Int -> PositivityCheck # fromEnum :: PositivityCheck -> Int # enumFrom :: PositivityCheck -> [PositivityCheck] # enumFromThen :: PositivityCheck -> PositivityCheck -> [PositivityCheck] # enumFromTo :: PositivityCheck -> PositivityCheck -> [PositivityCheck] # enumFromThenTo :: PositivityCheck -> PositivityCheck -> PositivityCheck -> [PositivityCheck] # | |||||
| Generic PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Associated Types
Methods from :: PositivityCheck -> Rep PositivityCheck x # to :: Rep PositivityCheck x -> PositivityCheck # | |||||
| Show PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> PositivityCheck -> ShowS # show :: PositivityCheck -> String # showList :: [PositivityCheck] -> ShowS # | |||||
| NFData PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: PositivityCheck -> () # | |||||
| Eq PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: PositivityCheck -> PositivityCheck -> Bool # (/=) :: PositivityCheck -> PositivityCheck -> Bool # | |||||
| Ord PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: PositivityCheck -> PositivityCheck -> Ordering # (<) :: PositivityCheck -> PositivityCheck -> Bool # (<=) :: PositivityCheck -> PositivityCheck -> Bool # (>) :: PositivityCheck -> PositivityCheck -> Bool # (>=) :: PositivityCheck -> PositivityCheck -> Bool # max :: PositivityCheck -> PositivityCheck -> PositivityCheck # min :: PositivityCheck -> PositivityCheck -> PositivityCheck # | |||||
| type Rep PositivityCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
Universe checking
data UniverseCheck Source #
Universe check? (Default is yes).
Constructors
| YesUniverseCheck | |
| NoUniverseCheck |
Instances
| KillRange UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| Bounded UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: UniverseCheck -> UniverseCheck # pred :: UniverseCheck -> UniverseCheck # toEnum :: Int -> UniverseCheck # fromEnum :: UniverseCheck -> Int # enumFrom :: UniverseCheck -> [UniverseCheck] # enumFromThen :: UniverseCheck -> UniverseCheck -> [UniverseCheck] # enumFromTo :: UniverseCheck -> UniverseCheck -> [UniverseCheck] # enumFromThenTo :: UniverseCheck -> UniverseCheck -> UniverseCheck -> [UniverseCheck] # | |||||
| Generic UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> UniverseCheck -> ShowS # show :: UniverseCheck -> String # showList :: [UniverseCheck] -> ShowS # | |||||
| NFData UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: UniverseCheck -> () # | |||||
| Eq UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: UniverseCheck -> UniverseCheck -> Bool # (/=) :: UniverseCheck -> UniverseCheck -> Bool # | |||||
| Ord UniverseCheck Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: UniverseCheck -> UniverseCheck -> Ordering # (<) :: UniverseCheck -> UniverseCheck -> Bool # (<=) :: UniverseCheck -> UniverseCheck -> Bool # (>) :: UniverseCheck -> UniverseCheck -> Bool # (>=) :: UniverseCheck -> UniverseCheck -> Bool # max :: UniverseCheck -> UniverseCheck -> UniverseCheck # min :: UniverseCheck -> UniverseCheck -> UniverseCheck # | |||||
| type Rep UniverseCheck Source # | |||||
Universe checking
data CoverageCheck Source #
Coverage check? (Default is yes).
Constructors
| YesCoverageCheck | |
| NoCoverageCheck |
Instances
| KillRange CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods | |||||
| Monoid CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods mempty :: CoverageCheck # mappend :: CoverageCheck -> CoverageCheck -> CoverageCheck # mconcat :: [CoverageCheck] -> CoverageCheck # | |||||
| Semigroup CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods (<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck # sconcat :: NonEmpty CoverageCheck -> CoverageCheck # stimes :: Integral b => b -> CoverageCheck -> CoverageCheck # | |||||
| Bounded CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common | |||||
| Enum CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods succ :: CoverageCheck -> CoverageCheck # pred :: CoverageCheck -> CoverageCheck # toEnum :: Int -> CoverageCheck # fromEnum :: CoverageCheck -> Int # enumFrom :: CoverageCheck -> [CoverageCheck] # enumFromThen :: CoverageCheck -> CoverageCheck -> [CoverageCheck] # enumFromTo :: CoverageCheck -> CoverageCheck -> [CoverageCheck] # enumFromThenTo :: CoverageCheck -> CoverageCheck -> CoverageCheck -> [CoverageCheck] # | |||||
| Generic CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
| Show CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> CoverageCheck -> ShowS # show :: CoverageCheck -> String # showList :: [CoverageCheck] -> ShowS # | |||||
| NFData CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods rnf :: CoverageCheck -> () # | |||||
| Eq CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods (==) :: CoverageCheck -> CoverageCheck -> Bool # (/=) :: CoverageCheck -> CoverageCheck -> Bool # | |||||
| Ord CoverageCheck Source # | |||||
Defined in Agda.Syntax.Common Methods compare :: CoverageCheck -> CoverageCheck -> Ordering # (<) :: CoverageCheck -> CoverageCheck -> Bool # (<=) :: CoverageCheck -> CoverageCheck -> Bool # (>) :: CoverageCheck -> CoverageCheck -> Bool # (>=) :: CoverageCheck -> CoverageCheck -> Bool # max :: CoverageCheck -> CoverageCheck -> CoverageCheck # min :: CoverageCheck -> CoverageCheck -> CoverageCheck # | |||||
| type Rep CoverageCheck Source # | |||||
Rewrite Directives on the LHS
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
Instances
| ToAbstract RewriteEqn Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source # | |||||
| Foldable (RewriteEqn' qn nm p) Source # | |||||
Defined in Agda.Syntax.Common Methods fold :: Monoid m => RewriteEqn' qn nm p m -> m # foldMap :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m # foldMap' :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m # foldr :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b # foldr' :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b # foldl :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b # foldl' :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b # foldr1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a # foldl1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a # toList :: RewriteEqn' qn nm p a -> [a] # null :: RewriteEqn' qn nm p a -> Bool # length :: RewriteEqn' qn nm p a -> Int # elem :: Eq a => a -> RewriteEqn' qn nm p a -> Bool # maximum :: Ord a => RewriteEqn' qn nm p a -> a # minimum :: Ord a => RewriteEqn' qn nm p a -> a # sum :: Num a => RewriteEqn' qn nm p a -> a # product :: Num a => RewriteEqn' qn nm p a -> a # | |||||
| Traversable (RewriteEqn' qn nm p) Source # | |||||
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> RewriteEqn' qn nm p a -> f (RewriteEqn' qn nm p b) # sequenceA :: Applicative f => RewriteEqn' qn nm p (f a) -> f (RewriteEqn' qn nm p a) # mapM :: Monad m => (a -> m b) -> RewriteEqn' qn nm p a -> m (RewriteEqn' qn nm p b) # sequence :: Monad m => RewriteEqn' qn nm p (m a) -> m (RewriteEqn' qn nm p a) # | |||||
| 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 # (<$) :: a -> RewriteEqn' qn nm p b -> RewriteEqn' qn nm p a # | |||||
| (ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Abstract.Views 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 # | |||||
| (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 :: RewriteEqn' qn BindName p a -> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a)) Source # bindToConcrete :: RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> AbsToCon b) -> AbsToCon b Source # | |||||
| ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) 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 # | |||||
| (Show e, Show qn, Show nm, Show p) => Show (RewriteEqn' qn nm p e) Source # | |||||
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> RewriteEqn' qn nm p e -> ShowS # show :: RewriteEqn' qn nm p e -> String # showList :: [RewriteEqn' qn nm p e] -> ShowS # | |||||
| (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 -> () # | |||||
| (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 # (/=) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool # | |||||
| type AbsOfCon RewriteEqn Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
| type ConOfAbs (RewriteEqn' qn BindName p a) Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete | |||||
| type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |||||
Information on expanded ellipsis (...)
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 | |
| Monoid ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods mappend :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis # mconcat :: [ExpandedEllipsis] -> ExpandedEllipsis # | |
| Semigroup ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis # sconcat :: NonEmpty ExpandedEllipsis -> ExpandedEllipsis # stimes :: Integral b => b -> ExpandedEllipsis -> ExpandedEllipsis # | |
| Show ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ExpandedEllipsis -> ShowS # show :: ExpandedEllipsis -> String # showList :: [ExpandedEllipsis] -> ShowS # | |
| NFData ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods rnf :: ExpandedEllipsis -> () # | |
| Eq ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods (==) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool # (/=) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool # | |
type Notation = [NotationPart] Source #
Notation as provided by the syntax declaration.
data BoundVariablePosition Source #
Positions of variables in syntax declarations.
Constructors
| BoundVariablePosition | |
Fields
| |
Instances
| EmbPrj BoundVariablePosition Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common | |
| Show BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> BoundVariablePosition -> ShowS # show :: BoundVariablePosition -> String # showList :: [BoundVariablePosition] -> ShowS # | |
| NFData BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common Methods rnf :: BoundVariablePosition -> () # | |
| Eq BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common Methods (==) :: BoundVariablePosition -> BoundVariablePosition -> Bool # (/=) :: BoundVariablePosition -> BoundVariablePosition -> Bool # | |
| Ord BoundVariablePosition Source # | |
Defined in Agda.Syntax.Common Methods compare :: BoundVariablePosition -> BoundVariablePosition -> Ordering # (<) :: BoundVariablePosition -> BoundVariablePosition -> Bool # (<=) :: BoundVariablePosition -> BoundVariablePosition -> Bool # (>) :: BoundVariablePosition -> BoundVariablePosition -> Bool # (>=) :: BoundVariablePosition -> BoundVariablePosition -> Bool # max :: BoundVariablePosition -> BoundVariablePosition -> BoundVariablePosition # min :: BoundVariablePosition -> BoundVariablePosition -> BoundVariablePosition # | |
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
| 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 | |
| Pretty NotationPart Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: NotationPart -> Doc Source # prettyPrec :: Int -> NotationPart -> Doc Source # prettyList :: [NotationPart] -> Doc Source # | |
| Show NotationPart Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> NotationPart -> ShowS # show :: NotationPart -> String # showList :: [NotationPart] -> ShowS # | |
| NFData NotationPart Source # | |
Defined in Agda.Syntax.Common Methods rnf :: NotationPart -> () # | |
| Eq NotationPart Source # | |
Defined in Agda.Syntax.Common | |
| Ord NotationPart Source # | |
Defined in Agda.Syntax.Common Methods compare :: NotationPart -> NotationPart -> Ordering # (<) :: NotationPart -> NotationPart -> Bool # (<=) :: NotationPart -> NotationPart -> Bool # (>) :: NotationPart -> NotationPart -> Bool # (>=) :: NotationPart -> NotationPart -> Bool # max :: NotationPart -> NotationPart -> NotationPart # min :: NotationPart -> NotationPart -> NotationPart # | |