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
- = UnknownFVs
- | KnownFVs IntSet
- unknownFreeVariables :: FreeVariables
- noFreeVariables :: FreeVariables
- oneFreeVariable :: Int -> FreeVariables
- freeVariablesFromList :: [Int] -> FreeVariables
- class LensFreeVariables a where
- getFreeVariables :: a -> FreeVariables
- setFreeVariables :: FreeVariables -> a -> a
- mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a
- hasNoFreeVariables :: LensFreeVariables a => a -> Bool
- 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 Word64
- noModuleNameHash :: ModuleNameHash
- data NameId = NameId !Word64 !ModuleNameHash
- newtype MetaId = MetaId {}
- 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 {
- ellipsisRange :: Range
- ellipsisWithArgs :: Int
- | NoEllipsis
- = ExpandedEllipsis {
- type Notation = [GenPart]
- noNotation :: Notation
- data GenPart
Documentation
Delayed
Used to specify whether something should be delayed.
Constructors
Delayed | |
NotDelayed |
Instances
Eq Delayed Source # | |
Data Delayed Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Delayed -> c Delayed gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Delayed dataTypeOf :: Delayed -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Delayed) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Delayed) gmapT :: (forall b. Data b => b -> b) -> Delayed -> Delayed gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r gmapQ :: (forall d. Data d => d -> u) -> Delayed -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Delayed -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed | |
Ord Delayed Source # | |
Show Delayed Source # | |
Generic Delayed Source # | |
NFData Delayed Source # | |
Defined in Agda.Syntax.Common | |
KillRange Delayed Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj Delayed Source # | |
type Rep Delayed Source # | |
Defined in Agda.Syntax.Common type Rep Delayed = D1 ('MetaData "Delayed" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Delayed" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotDelayed" 'PrefixI 'False) (U1 :: Type -> Type)) |
File
Constructors
AgdaFileType | |
MdFileType | |
RstFileType | |
TexFileType | |
OrgFileType |
Instances
Eq FileType Source # | |
Data FileType Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FileType -> c FileType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FileType toConstr :: FileType -> Constr dataTypeOf :: FileType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FileType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FileType) gmapT :: (forall b. Data b => b -> b) -> FileType -> FileType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FileType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FileType -> r gmapQ :: (forall d. Data d => d -> u) -> FileType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FileType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FileType -> m FileType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FileType -> m FileType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FileType -> m FileType | |
Ord FileType Source # | |
Defined in Agda.Syntax.Common | |
Show FileType Source # | |
Generic FileType Source # | |
NFData FileType Source # | |
Defined in Agda.Syntax.Common | |
Pretty FileType Source # | |
EmbPrj FileType Source # | |
type Rep FileType Source # | |
Defined in Agda.Syntax.Common type Rep FileType = D1 ('MetaData "FileType" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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.
Instances
Eq Cubical Source # | |
Show Cubical Source # | |
Generic Cubical Source # | |
NFData Cubical Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Cubical Source # | |
type Rep Cubical Source # | |
Defined in Agda.Syntax.Common type Rep Cubical = D1 ('MetaData "Cubical" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "CErased" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CFull" 'PrefixI 'False) (U1 :: Type -> Type)) |
Agda variants.
Only some variants are tracked.
Instances
Eq Language Source # | |
Show Language Source # | |
Generic Language Source # | |
NFData Language Source # | |
Defined in Agda.Syntax.Common | |
KillRange Language Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj Language Source # | |
type Rep Language Source # | |
Defined in Agda.Syntax.Common type Rep Language = D1 ('MetaData "Language" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "WithoutK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cubical" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cubical)))) |
Record Directives
data RecordDirectives' a Source #
Constructors
RecordDirectives | |
Fields
|
Instances
Functor RecordDirectives' Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> RecordDirectives' a -> RecordDirectives' b (<$) :: a -> RecordDirectives' b -> RecordDirectives' a # | |
DeclaredNames RecordDirectives Source # | |
Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RecordDirectives -> m Source # | |
Eq a => Eq (RecordDirectives' a) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: RecordDirectives' a -> RecordDirectives' a -> Bool (/=) :: RecordDirectives' a -> RecordDirectives' a -> Bool | |
Data a => Data (RecordDirectives' a) Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RecordDirectives' a -> c (RecordDirectives' a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RecordDirectives' a) toConstr :: RecordDirectives' a -> Constr dataTypeOf :: RecordDirectives' a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RecordDirectives' a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RecordDirectives' a)) gmapT :: (forall b. Data b => b -> b) -> RecordDirectives' a -> RecordDirectives' a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RecordDirectives' a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RecordDirectives' a -> r gmapQ :: (forall d. Data d => d -> u) -> RecordDirectives' a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RecordDirectives' a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RecordDirectives' a -> m (RecordDirectives' a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RecordDirectives' a -> m (RecordDirectives' a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RecordDirectives' a -> m (RecordDirectives' a) | |
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 -> () | |
KillRange a => KillRange (RecordDirectives' a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (RecordDirectives' a) Source # | |
HasRange a => HasRange (RecordDirectives' a) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: RecordDirectives' a -> Range Source # |
Eta-equality
Does a record come with eta-equality?
Instances
Functor HasEta' 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 # | |
CopatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: HasEta -> Bool Source # | |
PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
Eq a => Eq (HasEta' a) Source # | |
Data a => Data (HasEta' a) Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HasEta' a -> c (HasEta' a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (HasEta' a) toConstr :: HasEta' a -> Constr dataTypeOf :: HasEta' a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (HasEta' a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (HasEta' a)) gmapT :: (forall b. Data b => b -> b) -> HasEta' a -> HasEta' a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HasEta' a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HasEta' a -> r gmapQ :: (forall d. Data d => d -> u) -> HasEta' a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> HasEta' a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> HasEta' a -> m (HasEta' a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta' a -> m (HasEta' a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta' a -> m (HasEta' a) | |
Ord a => Ord (HasEta' a) Source # | |
Defined in Agda.Syntax.Common | |
Show a => Show (HasEta' a) Source # | |
NFData a => NFData (HasEta' a) Source # | |
Defined in Agda.Syntax.Common | |
KillRange a => KillRange (HasEta' a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (HasEta' a) Source # | |
HasRange a => HasRange (HasEta' a) Source # | |
EmbPrj a => EmbPrj (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
class PatternMatchingAllowed a where Source #
Can we pattern match on the record constructor?
Methods
patternMatchingAllowed :: a -> Bool Source #
Instances
PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: Induction -> Bool Source # | |
PatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
PatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
PatternMatchingAllowed EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods patternMatchingAllowed :: EtaEquality -> Bool Source # |
class CopatternMatchingAllowed a where Source #
Can we construct a record by copattern matching?
Methods
copatternMatchingAllowed :: a -> Bool Source #
Instances
CopatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
CopatternMatchingAllowed HasEta Source # | |
Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: HasEta -> Bool Source # | |
CopatternMatchingAllowed EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods copatternMatchingAllowed :: EtaEquality -> Bool Source # |
Induction
Inductive < Coinductive
Constructors
Inductive | |
CoInductive |
Instances
Eq Induction Source # | |
Data Induction Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Induction -> c Induction gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Induction toConstr :: Induction -> Constr dataTypeOf :: Induction -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Induction) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Induction) gmapT :: (forall b. Data b => b -> b) -> Induction -> Induction gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r gmapQ :: (forall d. Data d => d -> u) -> Induction -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Induction -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Induction -> m Induction gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction | |
Ord Induction Source # | |
Defined in Agda.Syntax.Common | |
Show Induction Source # | |
NFData Induction Source # | |
Defined in Agda.Syntax.Common | |
Pretty Induction Source # | |
KillRange Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange Induction Source # | |
PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: Induction -> Bool Source # | |
EmbPrj Induction Source # | |
Hiding
data Overlappable Source #
Constructors
YesOverlap | |
NoOverlap |
Instances
Eq Overlappable Source # | |
Defined in Agda.Syntax.Common | |
Data Overlappable Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Overlappable -> c Overlappable gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Overlappable toConstr :: Overlappable -> Constr dataTypeOf :: Overlappable -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Overlappable) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Overlappable) gmapT :: (forall b. Data b => b -> b) -> Overlappable -> Overlappable gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Overlappable -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Overlappable -> r gmapQ :: (forall d. Data d => d -> u) -> Overlappable -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Overlappable -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable | |
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 | |
Show Overlappable Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Overlappable -> ShowS show :: Overlappable -> String showList :: [Overlappable] -> ShowS | |
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 | |
Monoid Overlappable Source # | |
Defined in Agda.Syntax.Common Methods mappend :: Overlappable -> Overlappable -> Overlappable mconcat :: [Overlappable] -> Overlappable | |
NFData Overlappable Source # | |
Defined in Agda.Syntax.Common Methods rnf :: Overlappable -> () |
Constructors
Hidden | |
Instance Overlappable | |
NotHidden |
Instances
Eq Hiding Source # | |
Data Hiding Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Hiding -> c Hiding gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Hiding dataTypeOf :: Hiding -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Hiding) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Hiding) gmapT :: (forall b. Data b => b -> b) -> Hiding -> Hiding gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r gmapQ :: (forall d. Data d => d -> u) -> Hiding -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Hiding -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding | |
Ord Hiding Source # | |
Show Hiding Source # | |
Semigroup Hiding Source # |
|
Monoid Hiding Source # | |
NFData Hiding Source # | |
Defined in Agda.Syntax.Common | |
Pretty Hiding Source # | |
KillRange Hiding Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange Hiding Source # | |
LensHiding Hiding Source # | |
EmbPrj Hiding Source # | |
ChooseFlex Hiding Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Hiding -> Hiding -> FlexChoice Source # | |
Unquote 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
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
mergeHiding :: LensHiding a => WithHiding a -> a Source #
Monoidal composition of Hiding
information in some data.
visible :: LensHiding a => a -> Bool Source #
NotHidden
arguments are visible
.
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
newtype UnderComposition t Source #
Type wrapper to indicate composition or multiplicative monoid/semigroup context.
Constructors
UnderComposition t |
Instances
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
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
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
Eq Q0Origin Source # | |
Data Q0Origin Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Q0Origin -> c Q0Origin gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Q0Origin toConstr :: Q0Origin -> Constr dataTypeOf :: Q0Origin -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Q0Origin) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q0Origin) gmapT :: (forall b. Data b => b -> b) -> Q0Origin -> Q0Origin gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q0Origin -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q0Origin -> r gmapQ :: (forall d. Data d => d -> u) -> Q0Origin -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Q0Origin -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Q0Origin -> m Q0Origin gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Q0Origin -> m Q0Origin gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Q0Origin -> m Q0Origin | |
Ord Q0Origin Source # | |
Defined in Agda.Syntax.Common | |
Show Q0Origin Source # | |
Generic Q0Origin Source # | |
Semigroup Q0Origin Source # | Right-biased composition, because the left quantity acts as context, and the right one as occurrence. |
Monoid Q0Origin Source # | |
NFData Q0Origin Source # | |
Defined in Agda.Syntax.Common | |
Null Q0Origin Source # | |
Pretty Q0Origin Source # | |
KillRange Q0Origin Source # | |
Defined in Agda.Syntax.Common Methods | |
SetRange Q0Origin Source # | |
HasRange Q0Origin Source # | |
EmbPrj Q0Origin Source # | |
type Rep Q0Origin Source # | |
Defined in Agda.Syntax.Common type Rep Q0Origin = D1 ('MetaData "Q0Origin" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
Eq Q1Origin Source # | |
Data Q1Origin Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Q1Origin -> c Q1Origin gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Q1Origin toConstr :: Q1Origin -> Constr dataTypeOf :: Q1Origin -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Q1Origin) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q1Origin) gmapT :: (forall b. Data b => b -> b) -> Q1Origin -> Q1Origin gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q1Origin -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q1Origin -> r gmapQ :: (forall d. Data d => d -> u) -> Q1Origin -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Q1Origin -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Q1Origin -> m Q1Origin gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Q1Origin -> m Q1Origin gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Q1Origin -> m Q1Origin | |
Ord Q1Origin Source # | |
Defined in Agda.Syntax.Common | |
Show Q1Origin Source # | |
Generic Q1Origin Source # | |
Semigroup Q1Origin Source # | Right-biased composition, because the left quantity acts as context, and the right one as occurrence. |
Monoid Q1Origin Source # | |
NFData Q1Origin Source # | |
Defined in Agda.Syntax.Common | |
Null Q1Origin Source # | |
Pretty Q1Origin Source # | |
KillRange Q1Origin Source # | |
Defined in Agda.Syntax.Common Methods | |
SetRange Q1Origin Source # | |
HasRange Q1Origin Source # | |
EmbPrj Q1Origin Source # | |
type Rep Q1Origin Source # | |
Defined in Agda.Syntax.Common type Rep Q1Origin = D1 ('MetaData "Q1Origin" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
Eq QωOrigin Source # | |
Data QωOrigin Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QωOrigin -> c QωOrigin gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QωOrigin toConstr :: QωOrigin -> Constr dataTypeOf :: QωOrigin -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QωOrigin) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QωOrigin) gmapT :: (forall b. Data b => b -> b) -> QωOrigin -> QωOrigin gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QωOrigin -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QωOrigin -> r gmapQ :: (forall d. Data d => d -> u) -> QωOrigin -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> QωOrigin -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> QωOrigin -> m QωOrigin gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QωOrigin -> m QωOrigin gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QωOrigin -> m QωOrigin | |
Ord QωOrigin Source # | |
Defined in Agda.Syntax.Common | |
Show QωOrigin Source # | |
Generic QωOrigin Source # | |
Semigroup QωOrigin Source # | Right-biased composition, because the left quantity acts as context, and the right one as occurrence. |
Monoid QωOrigin Source # | |
NFData QωOrigin Source # | |
Defined in Agda.Syntax.Common | |
Null QωOrigin Source # | |
Pretty QωOrigin Source # | |
KillRange QωOrigin Source # | |
Defined in Agda.Syntax.Common Methods | |
SetRange QωOrigin Source # | |
HasRange QωOrigin Source # | |
EmbPrj QωOrigin Source # | |
type Rep QωOrigin Source # | |
Defined in Agda.Syntax.Common type Rep QωOrigin = D1 ('MetaData "Q\969Origin" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
Eq Quantity Source # | |
Data Quantity Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quantity -> c Quantity gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quantity toConstr :: Quantity -> Constr dataTypeOf :: Quantity -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quantity) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantity) gmapT :: (forall b. Data b => b -> b) -> Quantity -> Quantity gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r gmapQ :: (forall d. Data d => d -> u) -> Quantity -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Quantity -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity | |
Ord Quantity Source # | |
Defined in Agda.Syntax.Common | |
Show Quantity Source # | |
Generic Quantity Source # | |
NFData Quantity Source # | |
Defined in Agda.Syntax.Common | |
PartialOrd Quantity Source # | Note that the order is |
Defined in Agda.Syntax.Common Methods | |
Pretty Quantity Source # | |
KillRange Quantity Source # | |
Defined in Agda.Syntax.Common Methods | |
SetRange Quantity Source # | |
HasRange Quantity Source # | |
LensQuantity Quantity Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Quantity Source # | |
PrettyTCM Quantity Source # | |
Defined in Agda.TypeChecking.Pretty | |
Unquote Quantity Source # | |
Semigroup (UnderComposition Quantity) Source # | Composition of quantities (multiplication).
Right-biased for origin. |
Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity stimes :: Integral b => b -> 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 | |
Monoid (UnderComposition Quantity) Source # | In the absense of finite quantities besides 0, ω is the unit. Otherwise, 1 is the unit. |
Defined in Agda.Syntax.Common | |
Monoid (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Quantity mappend :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity mconcat :: [UnderAddition Quantity] -> UnderAddition Quantity | |
LeftClosedPOMonoid (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity Source # | |
POMonoid (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderComposition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderAddition Quantity) Source # | |
Defined in Agda.Syntax.Common | |
type Rep Quantity Source # | |
Defined in Agda.Syntax.Common type Rep Quantity = D1 ('MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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)))) |
sameQuantity :: Quantity -> Quantity -> Bool Source #
Equality ignoring 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
Erased.
A special case of Quantity
: erased or not.
Instances
Eq Erased Source # | |
Data Erased Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Erased -> c Erased gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Erased dataTypeOf :: Erased -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Erased) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Erased) gmapT :: (forall b. Data b => b -> b) -> Erased -> Erased gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Erased -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Erased -> r gmapQ :: (forall d. Data d => d -> u) -> Erased -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Erased -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Erased -> m Erased gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Erased -> m Erased gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Erased -> m Erased | |
Show Erased Source # | |
Generic Erased Source # | |
NFData Erased Source # | |
Defined in Agda.Syntax.Common | |
KillRange Erased Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange 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.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "Erased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q0Origin)) :+: C1 ('MetaCons "NotErased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QωOrigin))) |
defaultErased :: Erased Source #
The default value of type Erased
: not erased.
sameErased :: Erased -> Erased -> Bool Source #
Equality ignoring origin.
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
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
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
sameRelevance :: Relevance -> Relevance -> Bool Source #
Equality ignoring origin.
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
Eq Annotation Source # | |
Defined in Agda.Syntax.Common | |
Data Annotation Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annotation -> c Annotation gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Annotation toConstr :: Annotation -> Constr dataTypeOf :: Annotation -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Annotation) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annotation) gmapT :: (forall b. Data b => b -> b) -> Annotation -> Annotation gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annotation -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annotation -> r gmapQ :: (forall d. Data d => d -> u) -> Annotation -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Annotation -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annotation -> m Annotation gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotation -> m Annotation gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotation -> m Annotation | |
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 | |
Show Annotation Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Annotation -> ShowS show :: Annotation -> String showList :: [Annotation] -> ShowS | |
Generic Annotation Source # | |
Defined in Agda.Syntax.Common Associated Types type Rep Annotation :: Type -> Type | |
NFData Annotation Source # | |
Defined in Agda.Syntax.Common Methods rnf :: Annotation -> () | |
KillRange Annotation Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange Annotation Source # | |
Defined in Agda.Syntax.Common Methods getRange :: Annotation -> Range Source # | |
LensAnnotation Annotation Source # | |
Defined in Agda.Syntax.Common Methods getAnnotation :: Annotation -> Annotation Source # setAnnotation :: Annotation -> Annotation -> Annotation Source # mapAnnotation :: (Annotation -> Annotation) -> Annotation -> Annotation Source # | |
EmbPrj Annotation Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Annotation -> S Int32 Source # icod_ :: Annotation -> S Int32 Source # value :: Int32 -> R Annotation Source # | |
type Rep Annotation Source # | |
Defined in Agda.Syntax.Common type Rep Annotation = D1 ('MetaData "Annotation" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
Locks
Constructors
IsNotLock | |
IsLock | In the future there might be different kinds of them. For now we assume lock weakening. |
Instances
Bounded Lock Source # | |
Defined in Agda.Syntax.Common | |
Enum Lock Source # | |
Eq Lock Source # | |
Data Lock Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Lock -> c Lock gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Lock dataTypeOf :: Lock -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Lock) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Lock) gmapT :: (forall b. Data b => b -> b) -> Lock -> Lock gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Lock -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Lock -> r gmapQ :: (forall d. Data d => d -> u) -> Lock -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Lock -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Lock -> m Lock gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Lock -> m Lock gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Lock -> m Lock | |
Ord Lock Source # | |
Show Lock Source # | |
Generic Lock Source # | |
NFData Lock Source # | |
Defined in Agda.Syntax.Common | |
LensLock Lock Source # | |
EmbPrj Lock Source # | |
type Rep Lock Source # | |
Defined in Agda.Syntax.Common type Rep Lock = D1 ('MetaData "Lock" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "IsNotLock" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsLock" 'PrefixI 'False) (U1 :: Type -> Type)) |
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
Bounded Cohesion Source # | |
Defined in Agda.Syntax.Common | |
Enum Cohesion Source # | |
Defined in Agda.Syntax.Common | |
Eq Cohesion Source # | |
Data Cohesion Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Cohesion -> c Cohesion gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Cohesion toConstr :: Cohesion -> Constr dataTypeOf :: Cohesion -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Cohesion) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Cohesion) gmapT :: (forall b. Data b => b -> b) -> Cohesion -> Cohesion gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cohesion -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Cohesion -> r gmapQ :: (forall d. Data d => d -> u) -> Cohesion -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Cohesion -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Cohesion -> m Cohesion gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Cohesion -> m Cohesion gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Cohesion -> m Cohesion | |
Ord Cohesion Source # | Order is given by implication: flatter is smaller. |
Defined in Agda.Syntax.Common | |
Show Cohesion Source # | |
Generic Cohesion Source # | |
NFData Cohesion Source # | |
Defined in Agda.Syntax.Common | |
PartialOrd Cohesion Source # | Flatter is smaller. |
Defined in Agda.Syntax.Common Methods | |
Pretty Cohesion Source # | |
KillRange Cohesion Source # | |
Defined in Agda.Syntax.Common Methods | |
SetRange Cohesion Source # | |
HasRange Cohesion Source # | |
LensCohesion Cohesion Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Cohesion Source # | |
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 (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 | |
Monoid (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 | |
LeftClosedPOMonoid (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion Source # | |
POMonoid (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POMonoid (UnderAddition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderComposition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup (UnderAddition Cohesion) Source # | |
Defined in Agda.Syntax.Common | |
type Rep Cohesion Source # | |
Defined in Agda.Syntax.Common type Rep Cohesion = D1 ('MetaData "Cohesion" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
sameCohesion :: Cohesion -> Cohesion -> Bool Source #
Equality ignoring origin.
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
Eq Origin Source # | |
Data Origin Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Origin -> c Origin gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Origin dataTypeOf :: Origin -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Origin) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Origin) gmapT :: (forall b. Data b => b -> b) -> Origin -> Origin gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r gmapQ :: (forall d. Data d => d -> u) -> Origin -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Origin -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Origin -> m Origin gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin | |
Ord Origin Source # | |
Show Origin Source # | |
NFData Origin Source # | |
Defined in Agda.Syntax.Common | |
KillRange Origin Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange Origin Source # | |
LensOrigin Origin Source # | |
EmbPrj Origin Source # | |
ChooseFlex Origin Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Origin -> Origin -> FlexChoice Source # |
data WithOrigin a Source #
Decorating something with Origin
information.
Constructors
WithOrigin | |
Instances
Functor WithOrigin Source # | |
Defined in Agda.Syntax.Common | |
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) | |
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 # | |
MapNamedArgPattern NAP Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the |
Eq a => Eq (WithOrigin a) Source # | |
Defined in Agda.Syntax.Common | |
Data a => Data (WithOrigin a) Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WithOrigin a -> c (WithOrigin a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WithOrigin a) toConstr :: WithOrigin a -> Constr dataTypeOf :: WithOrigin a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WithOrigin a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WithOrigin a)) gmapT :: (forall b. Data b => b -> b) -> WithOrigin a -> WithOrigin a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithOrigin a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithOrigin a -> r gmapQ :: (forall d. Data d => d -> u) -> WithOrigin a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> WithOrigin a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a) | |
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 | |
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 -> () | |
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 # | |
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 # | |
HasRange a => HasRange (WithOrigin a) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: WithOrigin a -> Range 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 # | |
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 type PatternVarOut (NamedArg (Pattern' a)) Source # Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source # | |
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. |
EmbPrj a => EmbPrj (WithOrigin a) Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithOrigin a -> S Int32 Source # icod_ :: WithOrigin a -> S Int32 Source # value :: Int32 -> R (WithOrigin a) Source # | |
PrettyTCM (NamedArg Term) Source # | |
Defined in Agda.TypeChecking.Pretty | |
PrettyTCM (NamedArg Expr) 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 # | |
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |
Defined in Agda.TypeChecking.Rewriting.Clause | |
AddContext ([NamedArg Name], Type) Source # | |
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |
AddContext (List1 (NamedArg Name), Type) Source # | |
Defined in Agda.TypeChecking.Monad.Context | |
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
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
hasNoFreeVariables :: LensFreeVariables a => a -> Bool Source #
Argument decoration
A function argument can be hidden and/or irrelevant.
Constructors
ArgInfo | |
Fields
|
Instances
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
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 String Source # | |
Defined in Agda.Syntax.Common | |
Underscore ByteString Source # | |
Defined in Agda.Syntax.Common | |
Underscore Doc Source # | |
Defined in Agda.Syntax.Common | |
Underscore QName Source # | |
Defined in Agda.Syntax.Concrete.Name | |
Underscore Name Source # | |
Defined in Agda.Syntax.Concrete.Name | |
Underscore Expr Source # | |
Defined in Agda.Syntax.Abstract |
Named arguments
Something potentially carrying a name.
Constructors
Named | |
Fields
|
Instances
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
Functor 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 | |
Traversable Ranged Source # | |
Decoration Ranged Source # | |
MapNamedArgPattern NAP Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the |
Eq a => Eq (Ranged a) Source # | Ignores range. |
Data a => Data (Ranged a) Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ranged a -> c (Ranged a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ranged a) toConstr :: Ranged a -> Constr dataTypeOf :: Ranged a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Ranged a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ranged a)) gmapT :: (forall b. Data b => b -> b) -> Ranged a -> Ranged a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r gmapQ :: (forall d. Data d => d -> u) -> Ranged a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Ranged a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) | |
Ord a => Ord (Ranged a) Source # | Ignores range. |
Defined in Agda.Syntax.Common | |
Show a => Show (Ranged a) Source # | |
NFData a => NFData (Ranged a) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common | |
Pretty a => Pretty (Ranged a) Source # | Ignores range. |
Pretty e => Pretty (Named_ e) Source # | |
KillRange (Ranged a) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Ranged a) Source # | |
HasRange (Ranged a) Source # | |
IsNoName a => IsNoName (Ranged a) Source # | |
Defined in Agda.Syntax.Concrete.Name | |
PatternVars (NamedArg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (NamedArg (Pattern' a)) Source # Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source # | |
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. |
EmbPrj a => EmbPrj (Ranged a) Source # | |
PrettyTCM (NamedArg Term) Source # | |
Defined in Agda.TypeChecking.Pretty | |
PrettyTCM (NamedArg Expr) 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 # | |
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |
Defined in Agda.TypeChecking.Rewriting.Clause | |
AddContext ([NamedArg Name], Type) Source # | |
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |
AddContext (List1 (NamedArg Name), Type) Source # | |
Defined in Agda.TypeChecking.Monad.Context | |
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
Bounded ConOrigin Source # | |
Defined in Agda.Syntax.Common | |
Enum ConOrigin Source # | |
Defined in Agda.Syntax.Common | |
Eq ConOrigin Source # | |
Data ConOrigin Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConOrigin -> c ConOrigin gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConOrigin toConstr :: ConOrigin -> Constr dataTypeOf :: ConOrigin -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConOrigin) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConOrigin) gmapT :: (forall b. Data b => b -> b) -> ConOrigin -> ConOrigin gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r gmapQ :: (forall d. Data d => d -> u) -> ConOrigin -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ConOrigin -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin | |
Ord ConOrigin Source # | |
Defined in Agda.Syntax.Common | |
Show ConOrigin Source # | |
Generic ConOrigin Source # | |
NFData ConOrigin Source # | |
Defined in Agda.Syntax.Common | |
KillRange ConOrigin Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj ConOrigin Source # | |
type Rep ConOrigin Source # | |
Defined in Agda.Syntax.Common type Rep ConOrigin = D1 ('MetaData "ConOrigin" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
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] | |
Eq ProjOrigin Source # | |
Defined in Agda.Syntax.Common | |
Data ProjOrigin Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProjOrigin -> c ProjOrigin gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProjOrigin toConstr :: ProjOrigin -> Constr dataTypeOf :: ProjOrigin -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProjOrigin) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProjOrigin) gmapT :: (forall b. Data b => b -> b) -> ProjOrigin -> ProjOrigin gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProjOrigin -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProjOrigin -> r gmapQ :: (forall d. Data d => d -> u) -> ProjOrigin -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProjOrigin -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin | |
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 | |
Show ProjOrigin Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ProjOrigin -> ShowS show :: ProjOrigin -> String showList :: [ProjOrigin] -> ShowS | |
Generic ProjOrigin Source # | |
Defined in Agda.Syntax.Common Associated Types type Rep ProjOrigin :: Type -> Type | |
NFData ProjOrigin Source # | |
Defined in Agda.Syntax.Common Methods rnf :: ProjOrigin -> () | |
KillRange ProjOrigin Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj ProjOrigin Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ProjOrigin -> S Int32 Source # icod_ :: ProjOrigin -> S Int32 Source # value :: Int32 -> R ProjOrigin Source # | |
type Rep ProjOrigin Source # | |
Defined in Agda.Syntax.Common type Rep ProjOrigin = D1 ('MetaData "ProjOrigin" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
.
Instances
Eq IsInfix Source # | |
Data IsInfix Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsInfix -> c IsInfix gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInfix dataTypeOf :: IsInfix -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInfix) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInfix) gmapT :: (forall b. Data b => b -> b) -> IsInfix -> IsInfix gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r gmapQ :: (forall d. Data d => d -> u) -> IsInfix -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInfix -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix | |
Ord IsInfix Source # | |
Show IsInfix Source # | |
private blocks, public imports
Access modifier.
Constructors
PrivateAccess Origin | Store the |
PublicAccess |
Instances
Eq Access Source # | |
Data Access Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Access -> c Access gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Access dataTypeOf :: Access -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Access) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Access) gmapT :: (forall b. Data b => b -> b) -> Access -> Access gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r gmapQ :: (forall d. Data d => d -> u) -> Access -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Access -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Access -> m Access gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access | |
Ord Access Source # | |
Show Access Source # | |
NFData Access Source # | |
Defined in Agda.Syntax.Common | |
Pretty Access Source # | |
KillRange Access Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange Access Source # | |
EmbPrj Access Source # | |
abstract blocks
data IsAbstract Source #
Abstract or concrete.
Constructors
AbstractDef | |
ConcreteDef |
Instances
Eq IsAbstract Source # | |
Defined in Agda.Syntax.Common | |
Data IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsAbstract -> c IsAbstract gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsAbstract toConstr :: IsAbstract -> Constr dataTypeOf :: IsAbstract -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsAbstract) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsAbstract) gmapT :: (forall b. Data b => b -> b) -> IsAbstract -> IsAbstract gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsAbstract -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsAbstract -> r gmapQ :: (forall d. Data d => d -> u) -> IsAbstract -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> IsAbstract -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract | |
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 | |
Show IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsAbstract -> ShowS show :: IsAbstract -> String showList :: [IsAbstract] -> ShowS | |
Generic IsAbstract Source # | |
Defined in Agda.Syntax.Common Associated Types type Rep IsAbstract :: Type -> Type | |
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 | |
Monoid IsAbstract Source # | Default is |
Defined in Agda.Syntax.Common Methods mempty :: IsAbstract mappend :: IsAbstract -> IsAbstract -> IsAbstract mconcat :: [IsAbstract] -> IsAbstract | |
NFData IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods rnf :: IsAbstract -> () | |
KillRange IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods | |
AnyIsAbstract IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods anyIsAbstract :: IsAbstract -> IsAbstract Source # | |
LensIsAbstract IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj IsAbstract Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsAbstract -> S Int32 Source # icod_ :: IsAbstract -> S Int32 Source # value :: Int32 -> R IsAbstract Source # | |
type Rep IsAbstract Source # | |
Defined in Agda.Syntax.Common type Rep IsAbstract = D1 ('MetaData "IsAbstract" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "AbstractDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConcreteDef" 'PrefixI 'False) (U1 :: Type -> Type)) |
class LensIsAbstract a where Source #
Methods
lensIsAbstract :: Lens' IsAbstract a Source #
Instances
LensIsAbstract IsAbstract Source # | |
Defined in Agda.Syntax.Common Methods | |
LensIsAbstract TCEnv Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
LensIsAbstract MetaInfo 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 :: (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 a => AnyIsAbstract [a] Source # | |
Defined in Agda.Syntax.Common Methods anyIsAbstract :: [a] -> IsAbstract Source # | |
AnyIsAbstract a => AnyIsAbstract (Maybe a) Source # | |
Defined in Agda.Syntax.Common Methods anyIsAbstract :: Maybe a -> IsAbstract Source # | |
AnyIsAbstract (DefInfo' t) Source # | |
Defined in Agda.Syntax.Info Methods anyIsAbstract :: DefInfo' t -> IsAbstract Source # |
instance blocks
data IsInstance Source #
Is this definition eligible for instance search?
Constructors
InstanceDef Range | Range of the |
NotInstanceDef |
Instances
Eq IsInstance Source # | |
Defined in Agda.Syntax.Common | |
Data IsInstance Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsInstance -> c IsInstance gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInstance toConstr :: IsInstance -> Constr dataTypeOf :: IsInstance -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInstance) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInstance) gmapT :: (forall b. Data b => b -> b) -> IsInstance -> IsInstance gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInstance -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInstance -> r gmapQ :: (forall d. Data d => d -> u) -> IsInstance -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInstance -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance | |
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 | |
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 -> () | |
KillRange IsInstance Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange IsInstance Source # | |
Defined in Agda.Syntax.Common Methods getRange :: IsInstance -> Range Source # |
macro blocks
Is this a macro definition?
Constructors
MacroDef | |
NotMacroDef |
Instances
Eq IsMacro Source # | |
Data IsMacro Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsMacro -> c IsMacro gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsMacro dataTypeOf :: IsMacro -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsMacro) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsMacro) gmapT :: (forall b. Data b => b -> b) -> IsMacro -> IsMacro gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r gmapQ :: (forall d. Data d => d -> u) -> IsMacro -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> IsMacro -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro | |
Ord IsMacro Source # | |
Show IsMacro Source # | |
Generic IsMacro Source # | |
NFData IsMacro Source # | |
Defined in Agda.Syntax.Common | |
KillRange IsMacro Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange IsMacro Source # | |
type Rep IsMacro Source # | |
Defined in Agda.Syntax.Common type Rep IsMacro = D1 ('MetaData "IsMacro" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "MacroDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotMacroDef" 'PrefixI 'False) (U1 :: Type -> Type)) |
NameId
newtype ModuleNameHash Source #
Constructors
ModuleNameHash Word64 |
Instances
Eq ModuleNameHash Source # | |
Defined in Agda.Syntax.Common Methods (==) :: ModuleNameHash -> ModuleNameHash -> Bool (/=) :: ModuleNameHash -> ModuleNameHash -> Bool | |
Data ModuleNameHash Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleNameHash -> c ModuleNameHash gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleNameHash toConstr :: ModuleNameHash -> Constr dataTypeOf :: ModuleNameHash -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleNameHash) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleNameHash) gmapT :: (forall b. Data b => b -> b) -> ModuleNameHash -> ModuleNameHash gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleNameHash -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleNameHash -> r gmapQ :: (forall d. Data d => d -> u) -> ModuleNameHash -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleNameHash -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleNameHash -> m ModuleNameHash gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleNameHash -> m ModuleNameHash gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleNameHash -> m ModuleNameHash | |
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 | |
Show ModuleNameHash Source # | |
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 -> () | |
EmbPrj ModuleNameHash Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ModuleNameHash -> S Int32 Source # icod_ :: ModuleNameHash -> S Int32 Source # value :: Int32 -> R ModuleNameHash Source # |
The unique identifier of a name. Second argument is the top-level module identifier.
Constructors
NameId !Word64 !ModuleNameHash |
Instances
Enum NameId Source # | |
Defined in Agda.Syntax.Common | |
Eq NameId Source # | |
Data NameId Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameId -> c NameId gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameId dataTypeOf :: NameId -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameId) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameId) gmapT :: (forall b. Data b => b -> b) -> NameId -> NameId gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r gmapQ :: (forall d. Data d => d -> u) -> NameId -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> NameId -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameId -> m NameId gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId | |
Ord NameId Source # | |
Show NameId Source # | |
Generic NameId Source # | |
NFData NameId Source # | |
Defined in Agda.Syntax.Common | |
Hashable NameId Source # | |
Defined in Agda.Syntax.Common | |
Pretty NameId Source # | |
KillRange NameId Source # | |
Defined in Agda.Syntax.Common Methods | |
HasFresh NameId Source # | |
EmbPrj NameId 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.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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
A meta variable identifier is just a natural number.
Instances
Enum MetaId Source # | |
Defined in Agda.Syntax.Common | |
Eq MetaId Source # | |
Integral MetaId Source # | |
Data MetaId Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaId -> c MetaId gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaId dataTypeOf :: MetaId -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaId) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaId) gmapT :: (forall b. Data b => b -> b) -> MetaId -> MetaId gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r gmapQ :: (forall d. Data d => d -> u) -> MetaId -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaId -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId | |
Num MetaId Source # | |
Ord MetaId Source # | |
Real MetaId Source # | |
Defined in Agda.Syntax.Common Methods toRational :: MetaId -> Rational | |
Show MetaId Source # | Show non-record version of this newtype. |
Generic MetaId Source # | |
NFData MetaId Source # | |
Defined in Agda.Syntax.Common | |
Hashable MetaId Source # | |
Defined in Agda.Syntax.Common | |
Pretty MetaId Source # | |
GetDefs MetaId Source # | |
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => MetaId -> m () Source # | |
HasFresh MetaId Source # | |
EmbPrj MetaId Source # | |
PrettyTCM MetaId Source # | |
Defined in Agda.TypeChecking.Pretty | |
UnFreezeMeta MetaId Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source # | |
IsInstantiatedMeta MetaId Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source # | |
Reify MetaId Source # | |
FromTerm MetaId Source # | |
Defined in Agda.TypeChecking.Primitive | |
ToTerm MetaId Source # | |
PrimTerm MetaId Source # | |
PrimType MetaId Source # | |
Unquote MetaId Source # | |
ToJSON MetaId Source # | |
Defined in Agda.Interaction.JSONTop | |
EncodeTCM MetaId Source # | |
Singleton MetaId () Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
Singleton MetaId MetaSet Source # | |
type Rep MetaId Source # | |
Defined in Agda.Syntax.Common | |
type ReifiesTo MetaId Source # | |
Defined in Agda.Syntax.Translation.InternalToAbstract |
Constructors
Constr a |
Instances
ToConcrete (Constr Constructor) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Constr Constructor) Source # 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
Enum ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Eq ProblemId Source # | |
Integral ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Data ProblemId Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemId -> c ProblemId gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemId toConstr :: ProblemId -> Constr dataTypeOf :: ProblemId -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemId) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemId) gmapT :: (forall b. Data b => b -> b) -> ProblemId -> ProblemId gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r gmapQ :: (forall d. Data d => d -> u) -> ProblemId -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemId -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId | |
Num ProblemId Source # | |
Ord ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Real ProblemId Source # | |
Defined in Agda.Syntax.Common Methods toRational :: ProblemId -> Rational | |
Show ProblemId Source # | |
NFData ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Pretty ProblemId Source # | |
HasFresh ProblemId Source # | |
PrettyTCM ProblemId Source # | |
Defined in Agda.TypeChecking.Pretty | |
ToJSON ProblemId Source # | |
Defined in Agda.Interaction.JSONTop | |
EncodeTCM 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
Eq PositionInName Source # | |
Defined in Agda.Syntax.Common Methods (==) :: PositionInName -> PositionInName -> Bool (/=) :: PositionInName -> PositionInName -> Bool | |
Data PositionInName Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PositionInName -> c PositionInName gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PositionInName toConstr :: PositionInName -> Constr dataTypeOf :: PositionInName -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PositionInName) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PositionInName) gmapT :: (forall b. Data b => b -> b) -> PositionInName -> PositionInName gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r gmapQ :: (forall d. Data d => d -> u) -> PositionInName -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PositionInName -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName | |
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 | |
Show PositionInName Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> PositionInName -> ShowS show :: PositionInName -> String showList :: [PositionInName] -> ShowS |
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
noPlaceholder :: e -> MaybePlaceholder e Source #
An abbreviation: noPlaceholder =
.NoPlaceholder
Nothing
Interaction meta variables
newtype InteractionId Source #
Constructors
InteractionId | |
Fields
|
Instances
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
Eq FixityLevel Source # | |
Defined in Agda.Syntax.Common | |
Data FixityLevel Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FixityLevel -> c FixityLevel gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FixityLevel toConstr :: FixityLevel -> Constr dataTypeOf :: FixityLevel -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FixityLevel) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FixityLevel) gmapT :: (forall b. Data b => b -> b) -> FixityLevel -> FixityLevel gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FixityLevel -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FixityLevel -> r gmapQ :: (forall d. Data d => d -> u) -> FixityLevel -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FixityLevel -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel | |
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 | |
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 -> () | |
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 # | |
EmbPrj FixityLevel Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FixityLevel -> S Int32 Source # icod_ :: FixityLevel -> S Int32 Source # value :: Int32 -> R FixityLevel Source # | |
ToTerm FixityLevel Source # | |
Defined in Agda.TypeChecking.Primitive |
data Associativity Source #
Associativity.
Constructors
NonAssoc | |
LeftAssoc | |
RightAssoc |
Instances
Eq Associativity Source # | |
Defined in Agda.Syntax.Common | |
Data Associativity Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Associativity -> c Associativity gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Associativity toConstr :: Associativity -> Constr dataTypeOf :: Associativity -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Associativity) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Associativity) gmapT :: (forall b. Data b => b -> b) -> Associativity -> Associativity gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r gmapQ :: (forall d. Data d => d -> u) -> Associativity -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Associativity -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity | |
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 | |
Show Associativity Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Associativity -> ShowS show :: Associativity -> String showList :: [Associativity] -> ShowS | |
Pretty Associativity Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Associativity -> Doc Source # prettyPrec :: Int -> Associativity -> Doc Source # prettyList :: [Associativity] -> Doc Source # | |
EmbPrj Associativity Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Associativity -> S Int32 Source # icod_ :: Associativity -> S Int32 Source # value :: Int32 -> R Associativity Source # | |
ToTerm Associativity Source # | |
Defined in Agda.TypeChecking.Primitive |
Fixity of operators.
Constructors
Fixity | |
Fields
|
Instances
Eq Fixity Source # | |
Data Fixity Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity -> c Fixity gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity dataTypeOf :: Fixity -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity) gmapT :: (forall b. Data b => b -> b) -> Fixity -> Fixity gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r gmapQ :: (forall d. Data d => d -> u) -> Fixity -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity | |
Ord Fixity Source # | |
Show Fixity Source # | |
NFData Fixity Source # | |
Defined in Agda.Syntax.Common | |
Null Fixity Source # | |
Pretty Fixity Source # | |
KillRange Fixity Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange Fixity Source # | |
LensFixity Fixity Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Fixity Source # | |
ToTerm 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
Eq Fixity' Source # | |
Data Fixity' Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fixity' -> c Fixity' gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity' dataTypeOf :: Fixity' -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity') dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity') gmapT :: (forall b. Data b => b -> b) -> Fixity' -> Fixity' gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r gmapQ :: (forall d. Data d => d -> u) -> Fixity' -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity' -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' | |
Show Fixity' Source # | |
NFData Fixity' Source # | |
Defined in Agda.Syntax.Common | |
Null Fixity' Source # | |
Pretty Fixity' Source # | |
KillRange Fixity' Source # | |
Defined in Agda.Syntax.Common Methods | |
LensFixity' Fixity' Source # | |
Defined in Agda.Syntax.Common | |
LensFixity Fixity' Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Fixity' Source # | |
ToTerm Fixity' Source # | |
PrimTerm Fixity' Source # | |
PrimType Fixity' Source # | |
class LensFixity a where Source #
Methods
lensFixity :: Lens' Fixity a Source #
Instances
LensFixity Fixity' Source # | |
Defined in Agda.Syntax.Common | |
LensFixity Fixity Source # | |
Defined in Agda.Syntax.Common | |
LensFixity QName Source # | |
Defined in Agda.Syntax.Abstract.Name | |
LensFixity Name Source # | |
Defined in Agda.Syntax.Abstract.Name | |
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' Fixity' Source # | |
Defined in Agda.Syntax.Common | |
LensFixity' QName Source # | |
Defined in Agda.Syntax.Abstract.Name | |
LensFixity' Name Source # | |
Defined in Agda.Syntax.Abstract.Name | |
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
(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 | |
(Data n, Data m) => Data (ImportDirective' n m) Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImportDirective' n m -> c (ImportDirective' n m) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportDirective' n m) toConstr :: ImportDirective' n m -> Constr dataTypeOf :: ImportDirective' n m -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportDirective' n m)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportDirective' n m)) gmapT :: (forall b. Data b => b -> b) -> ImportDirective' n m -> ImportDirective' n m gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r gmapQ :: (forall d. Data d => d -> u) -> ImportDirective' n m -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportDirective' n m -> u gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) | |
(Show a, Show b) => Show (ImportDirective' a b) | |
Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ImportDirective' a b -> ShowS show :: ImportDirective' a b -> String showList :: [ImportDirective' a b] -> ShowS | |
(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 | |
(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 | |
(NFData a, NFData b) => NFData (ImportDirective' a b) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common Methods rnf :: ImportDirective' a b -> () | |
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 # | |
(KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportDirective' a b) Source # | |
(HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: ImportDirective' a b -> Range Source # |
type HidingDirective' n m = [ImportedName' n m] Source #
type RenamingDirective' n m = [Renaming' n m] Source #
defaultImportDir :: ImportDirective' n m Source #
Default is directive is private
(use everything, but do not export).
isDefaultImportDir :: ImportDirective' n m -> Bool Source #
isDefaultImportDir
implies null
, but not the other way round.
The using
clause of import directive.
Constructors
UseEverything | No |
Using [ImportedName' n m] |
|
Instances
(Eq m, Eq n) => Eq (Using' n m) Source # | |
(Data n, Data m) => Data (Using' n m) Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Using' n m -> c (Using' n m) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Using' n m) toConstr :: Using' n m -> Constr dataTypeOf :: Using' n m -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Using' n m)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Using' n m)) gmapT :: (forall b. Data b => b -> b) -> Using' n m -> Using' n m gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r gmapQ :: (forall d. Data d => d -> u) -> Using' n m -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Using' n m -> u gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) | |
(Show a, Show b) => Show (Using' a b) | |
Semigroup (Using' n m) Source # | |
Monoid (Using' n m) Source # | |
(NFData a, NFData b) => NFData (Using' a b) Source # | |
Defined in Agda.Syntax.Common | |
Null (Using' n m) Source # | |
(Pretty a, Pretty b) => Pretty (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 # | |
(HasRange a, HasRange b) => HasRange (Using' a b) 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
(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 | |
(Data n, Data m) => Data (ImportedName' n m) Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImportedName' n m -> c (ImportedName' n m) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportedName' n m) toConstr :: ImportedName' n m -> Constr dataTypeOf :: ImportedName' n m -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportedName' n m)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportedName' n m)) gmapT :: (forall b. Data b => b -> b) -> ImportedName' n m -> ImportedName' n m gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r gmapQ :: (forall d. Data d => d -> u) -> ImportedName' n m -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportedName' n m -> u gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) | |
(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 | |
(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 -> () | |
(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 # | |
(KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportedName' a b) Source # | |
(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: ImportedName' a b -> Range Source # | |
(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ImportedName' a b -> S Int32 Source # icod_ :: ImportedName' a b -> S Int32 Source # value :: Int32 -> R (ImportedName' a b) Source # |
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
(Eq m, Eq n) => Eq (Renaming' n m) Source # | |
(Data n, Data m) => Data (Renaming' n m) Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Renaming' n m -> c (Renaming' n m) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Renaming' n m) toConstr :: Renaming' n m -> Constr dataTypeOf :: Renaming' n m -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Renaming' n m)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Renaming' n m)) gmapT :: (forall b. Data b => b -> b) -> Renaming' n m -> Renaming' n m gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r gmapQ :: (forall d. Data d => d -> u) -> Renaming' n m -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Renaming' n m -> u gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) | |
(Show a, Show b) => Show (Renaming' a b) | |
(NFData a, NFData b) => NFData (Renaming' a b) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common | |
(Pretty a, Pretty b) => Pretty (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 # | |
(HasRange a, HasRange b) => HasRange (Renaming' a b) 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 # | |
Eq m => Eq (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: TerminationCheck m -> TerminationCheck m -> Bool (/=) :: TerminationCheck m -> TerminationCheck m -> Bool | |
Data m => Data (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TerminationCheck m -> c (TerminationCheck m) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TerminationCheck m) toConstr :: TerminationCheck m -> Constr dataTypeOf :: TerminationCheck m -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TerminationCheck m)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TerminationCheck m)) gmapT :: (forall b. Data b => b -> b) -> TerminationCheck m -> TerminationCheck m gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r gmapQ :: (forall d. Data d => d -> u) -> TerminationCheck m -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TerminationCheck m -> u gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) | |
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 -> () | |
KillRange m => KillRange (TerminationCheck m) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (TerminationCheck m) Source # |
Positivity
data PositivityCheck Source #
Positivity check? (Default = True).
Constructors
YesPositivityCheck | |
NoPositivityCheck |
Instances
Universe checking
data UniverseCheck Source #
Universe check? (Default is yes).
Constructors
YesUniverseCheck | |
NoUniverseCheck |
Instances
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] | |
Eq UniverseCheck Source # | |
Defined in Agda.Syntax.Common | |
Data UniverseCheck Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UniverseCheck -> c UniverseCheck gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UniverseCheck toConstr :: UniverseCheck -> Constr dataTypeOf :: UniverseCheck -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UniverseCheck) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UniverseCheck) gmapT :: (forall b. Data b => b -> b) -> UniverseCheck -> UniverseCheck gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r gmapQ :: (forall d. Data d => d -> u) -> UniverseCheck -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> UniverseCheck -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck | |
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 | |
Show UniverseCheck Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> UniverseCheck -> ShowS show :: UniverseCheck -> String showList :: [UniverseCheck] -> ShowS | |
Generic UniverseCheck Source # | |
Defined in Agda.Syntax.Common Associated Types type Rep UniverseCheck :: Type -> Type | |
NFData UniverseCheck Source # | |
Defined in Agda.Syntax.Common Methods rnf :: UniverseCheck -> () | |
KillRange UniverseCheck Source # | |
Defined in Agda.Syntax.Common Methods | |
type Rep UniverseCheck Source # | |
Defined in Agda.Syntax.Common type Rep UniverseCheck = D1 ('MetaData "UniverseCheck" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "YesUniverseCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoUniverseCheck" 'PrefixI 'False) (U1 :: Type -> Type)) |
Universe checking
data CoverageCheck Source #
Coverage check? (Default is yes).
Constructors
YesCoverageCheck | |
NoCoverageCheck |
Instances
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] | |
Eq CoverageCheck Source # | |
Defined in Agda.Syntax.Common | |
Data CoverageCheck Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoverageCheck -> c CoverageCheck gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoverageCheck toConstr :: CoverageCheck -> Constr dataTypeOf :: CoverageCheck -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoverageCheck) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoverageCheck) gmapT :: (forall b. Data b => b -> b) -> CoverageCheck -> CoverageCheck gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoverageCheck -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoverageCheck -> r gmapQ :: (forall d. Data d => d -> u) -> CoverageCheck -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CoverageCheck -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck | |
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 | |
Show CoverageCheck Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> CoverageCheck -> ShowS show :: CoverageCheck -> String showList :: [CoverageCheck] -> ShowS | |
Generic CoverageCheck Source # | |
Defined in Agda.Syntax.Common Associated Types type Rep CoverageCheck :: Type -> Type | |
Semigroup CoverageCheck Source # | |
Defined in Agda.Syntax.Common Methods (<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck # sconcat :: NonEmpty CoverageCheck -> CoverageCheck stimes :: Integral b => b -> CoverageCheck -> CoverageCheck | |
Monoid CoverageCheck Source # | |
Defined in Agda.Syntax.Common Methods mappend :: CoverageCheck -> CoverageCheck -> CoverageCheck mconcat :: [CoverageCheck] -> CoverageCheck | |
NFData CoverageCheck Source # | |
Defined in Agda.Syntax.Common Methods rnf :: CoverageCheck -> () | |
KillRange CoverageCheck Source # | |
Defined in Agda.Syntax.Common Methods | |
type Rep CoverageCheck Source # | |
Defined in Agda.Syntax.Common type Rep CoverageCheck = D1 ('MetaData "CoverageCheck" "Agda.Syntax.Common" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" 'False) (C1 ('MetaCons "YesCoverageCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoCoverageCheck" 'PrefixI 'False) (U1 :: Type -> Type)) |
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 type AbsOfCon RewriteEqn Source # Methods toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source # | |
Functor (RewriteEqn' qn nm p) Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> RewriteEqn' qn nm p a -> RewriteEqn' qn nm p b (<$) :: a -> RewriteEqn' qn nm p b -> RewriteEqn' qn nm p a # | |
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) | |
(Eq qn, Eq e, 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 | |
(Data qn, Data nm, Data p, Data e) => Data (RewriteEqn' qn nm p e) Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RewriteEqn' qn nm p e -> c (RewriteEqn' qn nm p e) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RewriteEqn' qn nm p e) toConstr :: RewriteEqn' qn nm p e -> Constr dataTypeOf :: RewriteEqn' qn nm p e -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RewriteEqn' qn nm p e)) dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RewriteEqn' qn nm p e)) gmapT :: (forall b. Data b => b -> b) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RewriteEqn' qn nm p e -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RewriteEqn' qn nm p e -> r gmapQ :: (forall d. Data d => d -> u) -> RewriteEqn' qn nm p e -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RewriteEqn' qn nm p e -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e) | |
(Show qn, Show e, 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 -> () | |
(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 # | |
(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 # | |
(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 # | |
(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 # | |
(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 # | |
(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (RewriteEqn' qn BindName p a) Source # 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 Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source # | |
type AbsOfCon RewriteEqn Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |
type ConOfAbs (RewriteEqn' qn BindName p a) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Information on expanded ellipsis (...
)
data ExpandedEllipsis Source #
Constructors
ExpandedEllipsis | |
Fields
| |
NoEllipsis |
Instances
Part of a Notation
Constructors
BindHole Range (Ranged Int) | Argument is the position of the hole (with binding) where the binding should occur. First range is the rhs range and second is the binder. |
NormalHole Range (NamedArg (Ranged Int)) | Argument is where the expression should go. |
WildHole (Ranged Int) | An underscore in binding position. |
IdPart RString |
Instances
Eq GenPart Source # | |
Data GenPart Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GenPart -> c GenPart gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenPart dataTypeOf :: GenPart -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GenPart) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenPart) gmapT :: (forall b. Data b => b -> b) -> GenPart -> GenPart gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r gmapQ :: (forall d. Data d => d -> u) -> GenPart -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> GenPart -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart | |
Ord GenPart Source # | |
Show GenPart Source # | |
NFData GenPart Source # | |
Defined in Agda.Syntax.Common | |
Pretty GenPart Source # | |
KillRange GenPart Source # | |
Defined in Agda.Syntax.Common Methods | |
SetRange GenPart Source # | |
HasRange GenPart Source # | |
EmbPrj GenPart Source # | |