| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Common
Contents
- Delayed
- File
- Eta-equality
- Induction
- Hiding
- Modalities
- Quantities
- Relevance
- Origin of arguments (user-written, inserted or reflected)
- Free variable annotations
- Argument decoration
- Arguments
- Names
- Function type domain
- 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
- Import directive
- Termination
- Positivity
- Universe checking
Description
Some common syntactic entities are defined in this module.
Synopsis
- 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
- lModRelevance :: Lens' Relevance Modality
- lModQuantity :: Lens' Quantity 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
- data Quantity
- defaultQuantity :: Quantity
- moreQuantity :: Quantity -> Quantity -> Bool
- usableQuantity :: LensQuantity a => a -> Bool
- composeQuantity :: Quantity -> Quantity -> Quantity
- applyQuantity :: LensQuantity a => Quantity -> a -> a
- inverseComposeQuantity :: Quantity -> Quantity -> Quantity
- inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a
- 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
- 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
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToRel :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- data Origin
- data WithOrigin a = WithOrigin {}
- class LensOrigin a where
- data FreeVariables
- unknownFreeVariables :: FreeVariables
- noFreeVariables :: FreeVariables
- oneFreeVariable :: Int -> FreeVariables
- freeVariablesFromList :: [Int] -> FreeVariables
- class LensFreeVariables a where
- getFreeVariables :: a -> FreeVariables
- setFreeVariables :: FreeVariables -> a -> a
- mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a
- hasNoFreeVariables :: LensFreeVariables a => a -> Bool
- data ArgInfo = ArgInfo {}
- class LensArgInfo a where
- getArgInfo :: a -> ArgInfo
- setArgInfo :: ArgInfo -> a -> a
- mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a
- defaultArgInfo :: ArgInfo
- getHidingArgInfo :: LensArgInfo a => LensGet Hiding a
- setHidingArgInfo :: LensArgInfo a => LensSet Hiding a
- mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a
- getModalityArgInfo :: LensArgInfo a => LensGet Modality a
- setModalityArgInfo :: LensArgInfo a => LensSet Modality a
- mapModalityArgInfo :: LensArgInfo a => LensMap Modality a
- getOriginArgInfo :: LensArgInfo a => LensGet Origin a
- setOriginArgInfo :: LensArgInfo a => LensSet Origin a
- mapOriginArgInfo :: LensArgInfo a => LensMap Origin a
- getFreeVariablesArgInfo :: LensArgInfo a => LensGet FreeVariables a
- setFreeVariablesArgInfo :: LensArgInfo a => LensSet FreeVariables a
- mapFreeVariablesArgInfo :: LensArgInfo a => LensMap FreeVariables a
- 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 Dom e = Dom {}
- argFromDom :: Dom a -> Arg a
- namedArgFromDom :: Dom a -> NamedArg a
- domFromArg :: Arg a -> Dom a
- domFromNamedArg :: NamedArg a -> Dom a
- defaultDom :: a -> Dom a
- defaultArgDom :: ArgInfo -> a -> Dom a
- defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
- data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
- type Named_ = Named RString
- unnamed :: a -> Named name a
- named :: name -> a -> Named name 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
- 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
- setNamedArg :: NamedArg a -> b -> NamedArg b
- 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
- data IsInstance
- data IsMacro
- type Nat = Int
- type Arity = Nat
- 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
- data ImportDirective' n m = ImportDirective {
- importDirRange :: Range
- using :: Using' n m
- hiding :: [ImportedName' n m]
- impRenaming :: [Renaming' n m]
- publicOpen :: Bool
- data Using' n m
- = UseEverything
- | Using [ImportedName' n m]
- defaultImportDir :: ImportDirective' n m
- isDefaultImportDir :: ImportDirective' n m -> Bool
- 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
- renToRange :: Range
- data TerminationCheck m
- type PositivityCheck = Bool
- data UniverseCheck
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 # toConstr :: Delayed -> Constr # 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 :: (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 :: (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 # toConstr :: HasEta -> Constr # 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 :: (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 :: (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 # | |
| 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
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 # toConstr :: Hiding -> Constr # 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 :: (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 one of setHiding or mapHiding.
Minimal complete definition
Instances
mergeHiding :: LensHiding a => WithHiding a -> a Source #
Monoidal composition of Hiding information in some data.
notVisible :: LensHiding a => a -> Bool Source #
:: LensHiding a => a -> Bool Source #
Hidden arguments are hidden.
hide :: LensHiding a => a -> a Source #
hideOrKeepInstance :: LensHiding a => a -> a Source #
makeInstance :: LensHiding a => a -> a Source #
makeInstance' :: LensHiding a => Overlappable -> a -> a Source #
isOverlappable :: LensHiding a => a -> Bool Source #
isInstance :: LensHiding a => a -> Bool Source #
sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool Source #
Ignores Overlappable.
Modalities
We have a tuple of modalities, which might not be fully orthogonal. For instance, irrelevant stuff is also run-time irrelevant.
Constructors
| Modality | |
Fields
| |
Instances
moreUsableModality :: Modality -> Modality -> Bool Source #
m means that an moreUsableModality m'm can be used
where ever an m' is required.
usableModality :: LensModality a => a -> Bool Source #
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.
class LensModality a where Source #
Minimal complete definition
Methods
getModality :: a -> Modality Source #
setModality :: Modality -> a -> a Source #
mapModality :: (Modality -> Modality) -> a -> a Source #
Instances
| LensModality ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
| LensModality Modality Source # | |
Defined in Agda.Syntax.Common | |
| LensModality (Dom e) Source # | |
Defined in Agda.Syntax.Common | |
| LensModality (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
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 #
Quantities
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 | Zero uses |
| Quantity1 | Linear use |
| Quantityω | Unrestricted use |
Instances
| Bounded Quantity Source # | |
| Enum Quantity Source # | |
Defined in Agda.Syntax.Common | |
| 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 :: (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). |
| 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 | |
| KillRange Quantity Source # | |
Defined in Agda.Syntax.Common Methods | |
| LensQuantity Quantity Source # | |
Defined in Agda.Syntax.Common | |
| EmbPrj Quantity Source # | |
| type Rep Quantity Source # | |
Defined in Agda.Syntax.Common type Rep Quantity = D1 (MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.0.1-FLv9kVJ1Yws5ccRin1RgxN" False) (C1 (MetaCons "Quantity0" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Quantity1" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Quantity\969" PrefixI False) (U1 :: Type -> Type))) | |
moreQuantity :: Quantity -> Quantity -> Bool Source #
m means that an moreUsableQuantity m'm can be used
where ever an m' is required.
usableQuantity :: LensQuantity a => a -> Bool Source #
A thing of quantity 0 is unusable, all others are usable.
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.
class LensQuantity a where Source #
Minimal complete definition
Methods
getQuantity :: a -> Quantity Source #
setQuantity :: Quantity -> a -> a Source #
mapQuantity :: (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 (Dom e) Source # | |
Defined in Agda.Syntax.Common | |
| LensQuantity (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
Relevance
A function argument can be relevant or irrelevant. See Agda.TypeChecking.Irrelevance.
Constructors
| Relevant | The argument is (possibly) relevant at compile-time. |
| NonStrict | The argument may never flow into evaluation position. Therefore, it is irrelevant at run-time. It is treated relevantly during equality checking. |
| Irrelevant | The argument is irrelevant at compile- and runtime. |
Instances
allRelevances :: [Relevance] Source #
class LensRelevance a where Source #
A lens to access the Relevance attribute in data structures.
Minimal implementation: getRelevance and one of setRelevance or mapRelevance.
Minimal complete definition
Methods
getRelevance :: a -> Relevance Source #
setRelevance :: Relevance -> a -> a Source #
mapRelevance :: (Relevance -> Relevance) -> a -> a Source #
Instances
| LensRelevance ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
| LensRelevance Relevance Source # | |
Defined in Agda.Syntax.Common | |
| LensRelevance Modality Source # | |
Defined in Agda.Syntax.Common | |
| LensRelevance TypedBinding Source # | |
Defined in Agda.Syntax.Concrete Methods getRelevance :: TypedBinding -> Relevance Source # setRelevance :: Relevance -> TypedBinding -> TypedBinding Source # mapRelevance :: (Relevance -> Relevance) -> TypedBinding -> TypedBinding Source # | |
| LensRelevance VarOcc Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
| LensRelevance (Dom e) Source # | |
Defined in Agda.Syntax.Common | |
| LensRelevance (Arg e) Source # | |
Defined in Agda.Syntax.Common | |
isRelevant :: LensRelevance a => a -> Bool Source #
isIrrelevant :: LensRelevance a => a -> Bool Source #
isNonStrict :: LensRelevance a => a -> Bool Source #
moreRelevant :: Relevance -> Relevance -> Bool Source #
Information ordering.
Relevant `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
usableRelevance :: LensRelevance a => a -> Bool Source #
usableRelevance rel == False iff we cannot use a variable of rel.
composeRelevance :: Relevance -> Relevance -> Relevance Source #
Relevance composition.
Irrelevant is dominant, Relevant is neutral.
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.
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 #
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 # toConstr :: Origin -> Constr # 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 :: (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 one of setOrigin or mapOrigin.
Minimal complete definition
Instances
| LensOrigin ArgInfo Source # | |
| LensOrigin Origin Source # | |
| LensOrigin AppInfo Source # | |
| LensOrigin (Dom e) 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 # | |
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 one of setFreeVariables or mapFreeVariables.
Minimal complete definition
Methods
getFreeVariables :: a -> FreeVariables Source #
setFreeVariables :: FreeVariables -> a -> a Source #
mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a Source #
Instances
hasNoFreeVariables :: LensFreeVariables a => a -> Bool Source #
Argument decoration
A function argument can be hidden and/or irrelevant.
Constructors
| ArgInfo | |
Fields | |
Instances
class LensArgInfo a where Source #
Minimal complete definition
Methods
getArgInfo :: a -> ArgInfo Source #
setArgInfo :: ArgInfo -> a -> a Source #
mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a Source #
Instances
| LensArgInfo ArgInfo Source # | |
Defined in Agda.Syntax.Common | |
| LensArgInfo (Dom e) Source # | |
Defined in Agda.Syntax.Common | |
| LensArgInfo (Arg a) Source # | |
Defined in Agda.Syntax.Common | |
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 #
Arguments
Instances
defaultArg :: a -> Arg a Source #
withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] Source #
Names
class Eq a => Underscore a where Source #
Minimal complete definition
Instances
| Underscore String Source # | |
Defined in Agda.Syntax.Common | |
| Underscore ByteString Source # | |
Defined in Agda.Syntax.Common | |
| Underscore Doc Source # | |
Defined in Agda.Syntax.Common | |
| Underscore QName Source # | |
Defined in Agda.Syntax.Concrete.Name | |
| Underscore Name Source # | |
Defined in Agda.Syntax.Concrete.Name | |
| Underscore Expr Source # | |
Defined in Agda.Syntax.Abstract | |
Function type domain
Similar to Arg, but we need to distinguish
an irrelevance annotation in a function domain
(the domain itself is not irrelevant!)
from an irrelevant argument.
Dom is used in Pi of internal syntax, in Context and Telescope.
Arg is used for actual arguments (Var, Con, Def etc.)
and in Abstract syntax and other situations.
- cubical
- When
domFinite = Truefor the domain of aPitype, the elements should be compared by tabulating the domain type. Only supported in case the domain type is primIsOne, to obtain the correct equality for partial elements.
Instances
argFromDom :: Dom a -> Arg a Source #
namedArgFromDom :: Dom a -> NamedArg a Source #
domFromArg :: Arg a -> Dom a Source #
domFromNamedArg :: NamedArg a -> Dom a Source #
defaultDom :: a -> Dom a Source #
defaultArgDom :: ArgInfo -> a -> Dom a Source #
Named arguments
Something potentially carrying a name.
Constructors
| Named | |
Fields
| |
Instances
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.
setNamedArg :: NamedArg a -> b -> NamedArg b Source #
setNamedArg a b = updateNamedArg (const b) a
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 # foldr :: (a -> b -> b) -> b -> Ranged a -> b # foldr' :: (a -> b -> b) -> b -> Ranged a -> b # foldl :: (b -> a -> b) -> b -> Ranged a -> b # foldl' :: (b -> a -> b) -> b -> Ranged a -> b # foldr1 :: (a -> a -> a) -> Ranged a -> a # foldl1 :: (a -> a -> a) -> Ranged a -> a # elem :: Eq a => a -> Ranged a -> Bool # maximum :: Ord a => Ranged a -> a # minimum :: Ord a => Ranged a -> a # | |
| Traversable Ranged Source # | |
| Decoration Ranged Source # | |
| MapNamedArgPattern NAP Source # | |
Defined in Agda.Syntax.Abstract.Pattern | |
| UniverseBi Declaration (NamedArg Pattern) | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Pattern] | |
| UniverseBi Declaration (NamedArg LHSCore) | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] | |
| UniverseBi Declaration (NamedArg Expr) | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] | |
| UniverseBi Declaration (NamedArg BindName) | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] | |
| PatternVars a (NamedArg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal | |
| MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the |
| 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 :: (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 # | |
| 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 # | |
| NormaliseProjP a => NormaliseProjP (Named_ a) Source # | |
Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source # | |
| ToAbstract [Arg Term] [NamedArg Expr] Source # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
| ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
| AddContext ([NamedArg Name], Type) Source # | |
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm 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
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
data DataOrRecord Source #
Instances
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 # toConstr :: IsInfix -> Constr # 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 :: (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 # | |
Access modifier.
Constructors
| PrivateAccess Origin | Store the |
| PublicAccess | |
| OnlyQualified | Visible from outside, but not exported when opening the module Used for qualified constructors. |
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 # toConstr :: Access -> Constr # 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 :: (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 # | |
data IsAbstract Source #
Abstract or concrete
Constructors
| AbstractDef | |
| ConcreteDef |
Instances
data IsInstance Source #
Is this definition eligible for instance search?
Constructors
| InstanceDef | |
| NotInstanceDef |
Instances
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 # toConstr :: IsMacro -> Constr # 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 :: (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.
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 # toConstr :: NameId -> Constr # 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 :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r # gmapQ :: (forall d. Data d => d -> u) -> NameId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NameId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameId -> m NameId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId # | |
| Ord NameId Source # | |
| Show NameId Source # | |
| Generic NameId Source # | |
| NFData NameId Source # | |
Defined in Agda.Syntax.Common | |
| Hashable NameId Source # | |
Defined in Agda.Syntax.Common | |
| Pretty NameId Source # | |
| KillRange NameId Source # | |
Defined in Agda.Syntax.Common Methods | |
| HasFresh NameId Source # | |
| EmbPrj NameId Source # | |
| type Rep NameId Source # | |
Defined in Agda.Syntax.Common type Rep NameId = D1 (MetaData "NameId" "Agda.Syntax.Common" "Agda-2.6.0.1-FLv9kVJ1Yws5ccRin1RgxN" 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
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
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
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
Constructors
| UseEverything | |
| 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 :: (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) Source # | |
| Semigroup (Using' n m) Source # | |
| Monoid (Using' n m) Source # | |
| (NFData a, NFData b) => NFData (Using' a b) Source # | |
Defined in Agda.Syntax.Common | |
| (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 # | |
defaultImportDir :: ImportDirective' n m Source #
Default is directive is private (use everything, but do not export).
isDefaultImportDir :: ImportDirective' n m -> Bool 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
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 :: (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) Source # | |
| (NFData a, NFData b) => NFData (Renaming' a b) Source # | Ranges are not forced. |
Defined in Agda.Syntax.Common | |
| (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
Positivity
type PositivityCheck = Bool Source #
Positivity check? (Default = True).
Universe checking
data UniverseCheck Source #
Universe check? (Default is yes).
Constructors
| YesUniverseCheck | |
| NoUniverseCheck |