| 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 # | |