Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Common
Contents
- Delayed
- File
- Eta-equality
- Induction
- Hiding
- Modalities
- Quantities
- Relevance
- 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
- 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 HasEta
- 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
- data Modality = Modality {}
- defaultModality :: Modality
- moreUsableModality :: Modality -> Modality -> Bool
- usableModality :: LensModality a => a -> Bool
- composeModality :: Modality -> Modality -> Modality
- applyModality :: LensModality a => Modality -> a -> a
- inverseComposeModality :: Modality -> Modality -> Modality
- inverseApplyModality :: LensModality a => Modality -> a -> a
- addModality :: Modality -> Modality -> Modality
- zeroModality :: Modality
- topModality :: 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
- defaultQuantity :: Quantity
- sameQuantity :: Quantity -> Quantity -> Bool
- addQuantity :: Quantity -> Quantity -> Quantity
- zeroQuantity :: 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 Relevance
- allRelevances :: [Relevance]
- defaultRelevance :: 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
- topRelevance :: Relevance
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToRel :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- data Cohesion
- = Flat
- | Continuous
- | Squash
- allCohesions :: [Cohesion]
- defaultCohesion :: 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
- topCohesion :: 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
- named :: name -> a -> Named name a
- userNamed :: Ranged ArgName -> a -> Named_ a
- class LensNamed name a | a -> name where
- getNameOf :: LensNamed name a => a -> Maybe name
- setNameOf :: LensNamed name a => Maybe name -> a -> a
- mapNameOf :: LensNamed name a => (Maybe name -> Maybe name) -> a -> a
- bareNameOf :: LensNamed NamedName a => a -> Maybe ArgName
- bareNameWithDefault :: LensNamed NamedName a => ArgName -> a -> ArgName
- namedSame :: (LensNamed NamedName a, LensNamed NamedName b) => a -> b -> Bool
- fittingNamedArg :: (LensNamed NamedName arg, LensHiding arg, LensNamed NamedName dom, 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 DataOrRecord
- data IsInfix
- data Access
- data IsAbstract
- class LensIsAbstract a where
- class AnyIsAbstract a where
- anyIsAbstract :: a -> IsAbstract
- data IsInstance
- data IsMacro
- data NameId = NameId !Word64 !Word64
- newtype MetaId = MetaId {}
- newtype Constr a = Constr a
- 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 :: [ImportedName' n m]
- impRenaming :: [Renaming' n m]
- publicOpen :: Maybe Range
- 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
- setImportedName :: ImportedName' a a -> a -> ImportedName' a a
- 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 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 # | |
KillRange Delayed Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj Delayed Source # | |
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 # | |
Pretty FileType Source # | |
EmbPrj FileType Source # | |
Eta-equality
Instances
Eq HasEta Source # | |
Data HasEta 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 -> c HasEta gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HasEta dataTypeOf :: HasEta -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HasEta) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HasEta) gmapT :: (forall b. Data b => b -> b) -> HasEta -> HasEta gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HasEta -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HasEta -> r gmapQ :: (forall d. Data d => d -> u) -> HasEta -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> HasEta -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta | |
Ord HasEta Source # | |
Show HasEta Source # | |
NFData HasEta Source # | |
Defined in Agda.Syntax.Common | |
KillRange HasEta Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange HasEta Source # | |
EmbPrj HasEta Source # | |
Induction
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 # | |
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 | |
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
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
Eq Modality Source # | |
Data Modality Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Modality -> c Modality gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Modality toConstr :: Modality -> Constr dataTypeOf :: Modality -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Modality) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Modality) gmapT :: (forall b. Data b => b -> b) -> Modality -> Modality gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Modality -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Modality -> r gmapQ :: (forall d. Data d => d -> u) -> Modality -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Modality -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Modality -> m Modality gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Modality -> m Modality gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Modality -> m Modality | |
Ord Modality Source # | |
Defined in Agda.Syntax.Common | |
Show Modality Source # | |
Generic Modality Source # | |
Semigroup Modality Source # | Pointwise composition. |
Monoid Modality Source # | Pointwise unit. |
NFData Modality Source # | |
Defined in Agda.Syntax.Common | |
PartialOrd Modality Source # | Dominance ordering. |
Defined in Agda.Syntax.Common Methods | |
LeftClosedPOMonoid Modality Source # | |
Defined in Agda.Syntax.Common | |
POMonoid Modality Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup Modality Source # | |
Defined in Agda.Syntax.Common | |
KillRange Modality Source # | |
Defined in Agda.Syntax.Common Methods | |
LensCohesion Modality Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance Modality Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity Modality Source # | |
Defined in Agda.Syntax.Common | |
LensModality Modality Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Modality Source # | |
PrettyTCM Modality Source # | |
Defined in Agda.TypeChecking.Pretty | |
Unquote Modality Source # | |
IsVarSet () AllowedVar Source # | |
Defined in Agda.TypeChecking.MetaVars.Occurs Methods withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar Source # | |
type Rep Modality Source # | |
Defined in Agda.Syntax.Common type Rep Modality = D1 ('MetaData "Modality" "Agda.Syntax.Common" "Agda-2.6.1-9a6JYGaPOygCbEuG99EdWV" 'False) (C1 ('MetaCons "Modality" 'PrefixI 'True) (S1 ('MetaSel ('Just "modRelevance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Relevance) :*: (S1 ('MetaSel ('Just "modQuantity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Quantity) :*: S1 ('MetaSel ('Just "modCohesion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cohesion)))) |
moreUsableModality :: Modality -> Modality -> Bool Source #
m
means that an moreUsableModality
m'm
can be used
where ever an m'
is required.
usableModality :: LensModality a => a -> Bool Source #
composeModality :: Modality -> Modality -> Modality Source #
Multiplicative monoid (standard monoid).
applyModality :: LensModality a => Modality -> a -> a Source #
Compose with modality flag from the left.
This function is e.g. used to update the modality information
on pattern variables a
after a match against something of modality q
.
inverseComposeModality :: Modality -> Modality -> Modality Source #
inverseComposeModality r x
returns the least modality y
such that forall x
, y
we have
x `moreUsableModality` (r `composeModality` y)
iff
(r `inverseComposeModality` x) `moreUsableModality` y
(Galois connection).
inverseApplyModality :: LensModality a => Modality -> a -> a Source #
Left division by a Modality
.
Used e.g. to modify context when going into a m
argument.
topModality :: Modality Source #
Absorptive element under addition.
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.1-9a6JYGaPOygCbEuG99EdWV" '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.1-9a6JYGaPOygCbEuG99EdWV" '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.1-9a6JYGaPOygCbEuG99EdWV" '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 # | |
Semigroup Quantity Source # | Composition of quantities (multiplication).
Right-biased for origin. |
Monoid Quantity Source # | In the absense of finite quantities besides 0, ω is the unit. Otherwise, 1 is the unit. |
NFData Quantity Source # | |
Defined in Agda.Syntax.Common | |
PartialOrd Quantity Source # | Note that the order is |
Defined in Agda.Syntax.Common Methods | |
LeftClosedPOMonoid Quantity Source # | |
Defined in Agda.Syntax.Common | |
POMonoid Quantity Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup Quantity Source # | |
Defined in Agda.Syntax.Common | |
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 | |
UniverseBi Declaration Quantity Source # | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [Quantity] Source # | |
type Rep Quantity Source # | |
Defined in Agda.Syntax.Common type Rep Quantity = D1 ('MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.1-9a6JYGaPOygCbEuG99EdWV" '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.
topQuantity :: Quantity Source #
Absorptive element is ω.
moreQuantity :: Quantity -> Quantity -> Bool Source #
m
means that an moreUsableQuantity
m'm
can be used
where ever an m'
is required.
applyQuantity :: LensQuantity a => Quantity -> a -> a Source #
Compose with quantity flag from the left.
This function is e.g. used to update the quantity information
on pattern variables a
after a match against something of quantity q
.
inverseComposeQuantity :: Quantity -> Quantity -> Quantity Source #
inverseComposeQuantity r x
returns the least quantity y
such that forall x
, y
we have
x `moreQuantity` (r `composeQuantity` y)
iff
(r `inverseComposeQuantity` x) `moreQuantity` y
(Galois connection).
inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a Source #
Left division by a Quantity
.
Used e.g. to modify context when going into a q
argument.
hasQuantity0 :: LensQuantity a => a -> Bool Source #
Check for Quantity0
.
hasQuantity1 :: LensQuantity a => a -> Bool Source #
Check for Quantity1
.
hasQuantityω :: LensQuantity a => a -> Bool Source #
Check for Quantityω
.
noUserQuantity :: LensQuantity a => a -> Bool Source #
Did the user supply a quantity annotation?
usableQuantity :: LensQuantity a => a -> Bool Source #
A thing of quantity 0 is unusable, all others are usable.
class LensQuantity a where Source #
Minimal complete definition
Nothing
Methods
getQuantity :: a -> Quantity Source #
default getQuantity :: LensModality a => a -> Quantity Source #
setQuantity :: Quantity -> a -> a Source #
mapQuantity :: (Quantity -> Quantity) -> a -> a Source #
default mapQuantity :: LensModality a => (Quantity -> Quantity) -> a -> a Source #
Instances
LensQuantity ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity Quantity Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity Modality Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity TCEnv Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
LensQuantity Definition Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getQuantity :: Definition -> Quantity Source # setQuantity :: Quantity -> Definition -> Definition Source # mapQuantity :: (Quantity -> Quantity) -> Definition -> Definition Source # | |
LensQuantity (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity (VarOcc' a) Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
LensQuantity (Dom' t e) Source # | |
Defined in Agda.Syntax.Internal | |
LensQuantity (FreeEnv' a b c) Source # | |
Defined in Agda.TypeChecking.Free.Lazy |
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
Bounded Relevance Source # | |
Defined in Agda.Syntax.Common | |
Enum Relevance Source # | |
Defined in Agda.Syntax.Common | |
Eq Relevance Source # | |
Data Relevance Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Relevance -> c Relevance gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Relevance toConstr :: Relevance -> Constr dataTypeOf :: Relevance -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Relevance) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Relevance) gmapT :: (forall b. Data b => b -> b) -> Relevance -> Relevance gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Relevance -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Relevance -> r gmapQ :: (forall d. Data d => d -> u) -> Relevance -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Relevance -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance | |
Ord Relevance Source # | More relevant is smaller. |
Defined in Agda.Syntax.Common | |
Show Relevance Source # | |
Generic Relevance Source # | |
Semigroup Relevance Source # |
|
Monoid Relevance Source # |
|
NFData Relevance Source # | |
Defined in Agda.Syntax.Common | |
PartialOrd Relevance Source # | More relevant is smaller. |
Defined in Agda.Syntax.Common Methods | |
LeftClosedPOMonoid Relevance Source # | |
Defined in Agda.Syntax.Common | |
POMonoid Relevance Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup Relevance Source # | |
Defined in Agda.Syntax.Common | |
Pretty Relevance Source # | |
KillRange Relevance Source # | |
Defined in Agda.Syntax.Common Methods | |
SetRange Relevance Source # | |
HasRange Relevance Source # | |
LensRelevance Relevance Source # | |
Defined in Agda.Syntax.Common | |
EmbPrj Relevance Source # | |
PrettyTCM Relevance Source # | |
Defined in Agda.TypeChecking.Pretty | |
Unquote Relevance Source # | |
type Rep Relevance Source # | |
Defined in Agda.Syntax.Common type Rep Relevance = D1 ('MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.6.1-9a6JYGaPOygCbEuG99EdWV" 'False) (C1 ('MetaCons "Relevant" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonStrict" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Irrelevant" 'PrefixI 'False) (U1 :: Type -> Type))) |
allRelevances :: [Relevance] Source #
class LensRelevance a where Source #
A lens to access the Relevance
attribute in data structures.
Minimal implementation: getRelevance
and mapRelevance
or LensModality
.
Minimal complete definition
Nothing
Methods
getRelevance :: a -> Relevance Source #
default getRelevance :: LensModality a => a -> Relevance Source #
setRelevance :: Relevance -> a -> a Source #
mapRelevance :: (Relevance -> Relevance) -> a -> a Source #
default mapRelevance :: LensModality a => (Relevance -> Relevance) -> a -> a Source #
Instances
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.
topRelevance :: Relevance Source #
Absorptive element under addition.
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 #
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 # | |
Semigroup Cohesion Source # |
|
Monoid Cohesion Source # |
|
NFData Cohesion Source # | |
Defined in Agda.Syntax.Common | |
PartialOrd Cohesion Source # | Flatter is smaller. |
Defined in Agda.Syntax.Common Methods | |
LeftClosedPOMonoid Cohesion Source # | |
Defined in Agda.Syntax.Common | |
POMonoid Cohesion Source # | |
Defined in Agda.Syntax.Common | |
POSemigroup Cohesion Source # | |
Defined in Agda.Syntax.Common | |
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 # | |
type Rep Cohesion Source # | |
Defined in Agda.Syntax.Common type Rep Cohesion = D1 ('MetaData "Cohesion" "Agda.Syntax.Common" "Agda-2.6.1-9a6JYGaPOygCbEuG99EdWV" '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.
topCohesion :: Cohesion Source #
Absorptive element under addition.
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 | |
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
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
Eq ArgInfo Source # | |
Data ArgInfo Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ArgInfo -> c ArgInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ArgInfo dataTypeOf :: ArgInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ArgInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgInfo) gmapT :: (forall b. Data b => b -> b) -> ArgInfo -> ArgInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArgInfo -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArgInfo -> r gmapQ :: (forall d. Data d => d -> u) -> ArgInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ArgInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo | |
Ord ArgInfo Source # | |
Show ArgInfo Source # | |
NFData ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
KillRange ArgInfo Source # | |
Defined in Agda.Syntax.Common Methods | |
LensArgInfo ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensFreeVariables ArgInfo Source # | |
Defined in Agda.Syntax.Common Methods getFreeVariables :: ArgInfo -> FreeVariables Source # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo Source # | |
LensOrigin ArgInfo Source # | |
LensCohesion ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensRelevance ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensQuantity ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensModality ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
LensHiding ArgInfo Source # | |
EmbPrj ArgInfo Source # | |
SynEq ArgInfo Source # | |
ToTerm ArgInfo Source # | |
ChooseFlex ArgInfo Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: ArgInfo -> ArgInfo -> FlexChoice Source # | |
Unquote ArgInfo Source # | |
EqualSy ArgInfo Source # | Ignore origin and free variables. |
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 ByteString Source # | |
Defined in Agda.Syntax.Common | |
Underscore String 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 name a | a -> name where Source #
Accessor/editor for the nameOf
component.
Minimal complete definition
Nothing
Methods
fittingNamedArg :: (LensNamed NamedName arg, LensHiding arg, LensNamed NamedName dom, 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 | |
UniverseBi Declaration (NamedArg Pattern) Source # | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Pattern] Source # | |
UniverseBi Declaration (NamedArg LHSCore) Source # | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] Source # | |
UniverseBi Declaration (NamedArg Expr) Source # | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] Source # | |
UniverseBi Declaration (NamedArg BindName) Source # | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] Source # | |
PatternVars a (NamedArg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal | |
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the |
LensNamed NamedName (Dom' t e) Source # | |
Eq a => Eq (Ranged a) Source # | |
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 # | |
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 # | |
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 | |
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. |
EmbPrj a => EmbPrj (Ranged a) Source # | |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) 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 | |
ToAbstract [Arg Term] [NamedArg Expr] Source # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => [Arg Term] -> m [NamedArg Expr] Source # | |
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Arg r -> m (NamedArg a) Source # | |
AddContext ([NamedArg Name], Type) Source # | |
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # |
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 # | |
KillRange ConOrigin Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj ConOrigin Source # | |
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 | |
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 # |
data DataOrRecord Source #
Instances
Eq DataOrRecord Source # | |
Defined in Agda.Syntax.Common | |
Data DataOrRecord Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataOrRecord -> c DataOrRecord gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataOrRecord toConstr :: DataOrRecord -> Constr dataTypeOf :: DataOrRecord -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataOrRecord) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataOrRecord) gmapT :: (forall b. Data b => b -> b) -> DataOrRecord -> DataOrRecord gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r gmapQ :: (forall d. Data d => d -> u) -> DataOrRecord -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DataOrRecord -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord | |
Ord DataOrRecord Source # | |
Defined in Agda.Syntax.Common Methods compare :: DataOrRecord -> DataOrRecord -> Ordering (<) :: DataOrRecord -> DataOrRecord -> Bool (<=) :: DataOrRecord -> DataOrRecord -> Bool (>) :: DataOrRecord -> DataOrRecord -> Bool (>=) :: DataOrRecord -> DataOrRecord -> Bool max :: DataOrRecord -> DataOrRecord -> DataOrRecord min :: DataOrRecord -> DataOrRecord -> DataOrRecord | |
Show DataOrRecord Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> DataOrRecord -> ShowS show :: DataOrRecord -> String showList :: [DataOrRecord] -> ShowS | |
EmbPrj DataOrRecord Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: DataOrRecord -> S Int32 Source # icod_ :: DataOrRecord -> S Int32 Source # value :: Int32 -> R DataOrRecord Source # |
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 | |
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 | |
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 # |
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 # | |
KillRange IsMacro Source # | |
Defined in Agda.Syntax.Common Methods | |
HasRange IsMacro Source # | |
NameId
The unique identifier of a name. Second argument is the top-level module identifier.
Constructors
NameId !Word64 !Word64 |
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 # | |
Hashable NameId Source # | |
Defined in Agda.Syntax.Common | |
NFData 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.1-9a6JYGaPOygCbEuG99EdWV" '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 Word64))) |
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 # | |
Hashable MetaId Source # | |
Defined in Agda.Syntax.Common | |
NFData 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 # | |
FromTerm MetaId Source # | |
Defined in Agda.TypeChecking.Primitive | |
ToTerm MetaId Source # | |
PrimTerm MetaId Source # | |
Unquote MetaId Source # | |
Singleton MetaId () Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
Singleton MetaId MetaSet Source # | |
Reify MetaId Expr Source # | |
Defined in Agda.Syntax.Translation.InternalToAbstract | |
type Rep MetaId Source # | |
Defined in Agda.Syntax.Common |
Constructors
Constr a |
Instances
ToConcrete (Constr Constructor) Declaration Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Constr Constructor -> AbsToCon Declaration Source # bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b 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 | |
Null FixityLevel Source # | |
Defined in Agda.Syntax.Common | |
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 | |
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 # | |
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 | |
(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 # |
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 # |
setImportedName :: ImportedName' a a -> a -> ImportedName' a a Source #
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
Universe checking
data CoverageCheck Source #
Coverage check? (Default is yes).
Constructors
YesCoverageCheck | |
NoCoverageCheck |
Instances
Rewrite Directives on the LHS
data RewriteEqn' qn 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
p
is the type of patterns
e
is the type of expressions
Instances
ToAbstract RewriteEqn (RewriteEqn' () Pattern Expr) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RewriteEqn -> ScopeM (RewriteEqn' () Pattern Expr) Source # | |
ToConcrete RHS (RHS, [RewriteEqn], [WithHiding Expr], [Declaration]) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [RewriteEqn], [WithHiding Expr], [Declaration]) Source # bindToConcrete :: RHS -> ((RHS0, [RewriteEqn], [WithHiding Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b Source # | |
Functor (RewriteEqn' qn p) Source # | |
Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> RewriteEqn' qn p a -> RewriteEqn' qn p b (<$) :: a -> RewriteEqn' qn p b -> RewriteEqn' qn p a # | |
Foldable (RewriteEqn' qn p) Source # | |
Defined in Agda.Syntax.Common Methods fold :: Monoid m => RewriteEqn' qn p m -> m foldMap :: Monoid m => (a -> m) -> RewriteEqn' qn p a -> m foldMap' :: Monoid m => (a -> m) -> RewriteEqn' qn p a -> m foldr :: (a -> b -> b) -> b -> RewriteEqn' qn p a -> b foldr' :: (a -> b -> b) -> b -> RewriteEqn' qn p a -> b foldl :: (b -> a -> b) -> b -> RewriteEqn' qn p a -> b foldl' :: (b -> a -> b) -> b -> RewriteEqn' qn p a -> b foldr1 :: (a -> a -> a) -> RewriteEqn' qn p a -> a foldl1 :: (a -> a -> a) -> RewriteEqn' qn p a -> a toList :: RewriteEqn' qn p a -> [a] null :: RewriteEqn' qn p a -> Bool length :: RewriteEqn' qn p a -> Int elem :: Eq a => a -> RewriteEqn' qn p a -> Bool maximum :: Ord a => RewriteEqn' qn p a -> a minimum :: Ord a => RewriteEqn' qn p a -> a sum :: Num a => RewriteEqn' qn p a -> a product :: Num a => RewriteEqn' qn p a -> a | |
Traversable (RewriteEqn' qn p) Source # | |
Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> RewriteEqn' qn p a -> f (RewriteEqn' qn p b) sequenceA :: Applicative f => RewriteEqn' qn p (f a) -> f (RewriteEqn' qn p a) mapM :: Monad m => (a -> m b) -> RewriteEqn' qn p a -> m (RewriteEqn' qn p b) sequence :: Monad m => RewriteEqn' qn p (m a) -> m (RewriteEqn' qn p a) | |
(Eq qn, Eq e, Eq p) => Eq (RewriteEqn' qn p e) Source # | |
Defined in Agda.Syntax.Common Methods (==) :: RewriteEqn' qn p e -> RewriteEqn' qn p e -> Bool (/=) :: RewriteEqn' qn p e -> RewriteEqn' qn p e -> Bool | |
(Data qn, Data p, Data e) => Data (RewriteEqn' qn 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 p e -> c (RewriteEqn' qn p e) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RewriteEqn' qn p e) toConstr :: RewriteEqn' qn p e -> Constr dataTypeOf :: RewriteEqn' qn p e -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RewriteEqn' qn p e)) dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RewriteEqn' qn p e)) gmapT :: (forall b. Data b => b -> b) -> RewriteEqn' qn p e -> RewriteEqn' qn p e gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RewriteEqn' qn p e -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RewriteEqn' qn p e -> r gmapQ :: (forall d. Data d => d -> u) -> RewriteEqn' qn p e -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RewriteEqn' qn p e -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) | |
(Show qn, Show e, Show p) => Show (RewriteEqn' qn p e) Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> RewriteEqn' qn p e -> ShowS show :: RewriteEqn' qn p e -> String showList :: [RewriteEqn' qn p e] -> ShowS | |
(NFData qn, NFData p, NFData e) => NFData (RewriteEqn' qn p e) Source # | |
Defined in Agda.Syntax.Common Methods rnf :: RewriteEqn' qn p e -> () | |
(Pretty p, Pretty e) => Pretty (RewriteEqn' qn p e) Source # | |
Defined in Agda.Syntax.Common Methods pretty :: RewriteEqn' qn p e -> Doc Source # prettyPrec :: Int -> RewriteEqn' qn p e -> Doc Source # prettyList :: [RewriteEqn' qn p e] -> Doc Source # | |
(KillRange qn, KillRange e, KillRange p) => KillRange (RewriteEqn' qn p e) Source # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (RewriteEqn' qn p e) Source # | |
(HasRange qn, HasRange p, HasRange e) => HasRange (RewriteEqn' qn p e) Source # | |
Defined in Agda.Syntax.Common Methods getRange :: RewriteEqn' qn p e -> Range Source # | |
(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn p e) Source # | |
Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> RewriteEqn' qn p e -> RewriteEqn' qn p e Source # traverseExpr :: Monad m => (Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source # foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn p e -> m Source # | |
(AllNames qn, AllNames e) => AllNames (RewriteEqn' qn p e) Source # | |
Defined in Agda.Syntax.Abstract Methods allNames :: RewriteEqn' qn p e -> Seq QName Source # | |
(ExprLike qn, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn p e) Source # | |
Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source # foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn p e -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source # mapExpr :: (Expr -> Expr) -> RewriteEqn' qn p e -> RewriteEqn' qn p e Source # | |
ToAbstract (RewriteEqn' () Pattern Expr) RewriteEqn Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RewriteEqn' () Pattern Expr -> ScopeM RewriteEqn Source # | |
(ToConcrete p q, ToConcrete a b) => ToConcrete (RewriteEqn' qn p a) (RewriteEqn' () q b) Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RewriteEqn' qn p a -> AbsToCon (RewriteEqn' () q b) Source # bindToConcrete :: RewriteEqn' qn p a -> (RewriteEqn' () q b -> AbsToCon b0) -> AbsToCon b0 Source # |
Information on expanded ellipsis (...
)
data ExpandedEllipsis Source #
Constructors
ExpandedEllipsis | |
Fields
| |
NoEllipsis |
Instances
Eq ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods (==) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool (/=) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool | |
Data ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExpandedEllipsis -> c ExpandedEllipsis gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExpandedEllipsis toConstr :: ExpandedEllipsis -> Constr dataTypeOf :: ExpandedEllipsis -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExpandedEllipsis) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpandedEllipsis) gmapT :: (forall b. Data b => b -> b) -> ExpandedEllipsis -> ExpandedEllipsis gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExpandedEllipsis -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExpandedEllipsis -> r gmapQ :: (forall d. Data d => d -> u) -> ExpandedEllipsis -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ExpandedEllipsis -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis | |
Show ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ExpandedEllipsis -> ShowS show :: ExpandedEllipsis -> String showList :: [ExpandedEllipsis] -> ShowS | |
NFData ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods rnf :: ExpandedEllipsis -> () | |
Null ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common | |
KillRange ExpandedEllipsis Source # | |
Defined in Agda.Syntax.Common Methods | |
EmbPrj ExpandedEllipsis Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ExpandedEllipsis -> S Int32 Source # icod_ :: ExpandedEllipsis -> S Int32 Source # value :: Int32 -> R ExpandedEllipsis Source # |
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 # | |