Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

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
  - HasRange instances
  - KillRange instances
  - NFData instances
- Termination
- Positivity
- Universe checking

Description

Some common syntactic entities are defined in this module.

Synopsis

- data Delayed
  - = Delayed
  - | NotDelayed
- data FileType
  - = AgdaFileType
  - | MdFileType
  - | RstFileType
  - | TexFileType
  - | OrgFileType
- data HasEta
  - = NoEta
  - | YesEta
- data Induction
  - = Inductive
  - | CoInductive
- data Overlappable
  - = YesOverlap
  - | NoOverlap
- data Hiding
  - = Hidden
  - | Instance Overlappable
  - | NotHidden
- data WithHiding a = WithHiding {
  - whHiding :: !Hiding
  - whThing :: a
  }
- class LensHiding a where
  - getHiding :: a -> Hiding
  - setHiding :: Hiding -> a -> a
  - mapHiding :: (Hiding -> Hiding) -> a -> a
- 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 {
  - modRelevance :: Relevance
  - modQuantity :: Quantity
  }
- 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
  - = Quantity0
  - | Quantity1
  - | 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
  - = Relevant
  - | NonStrict
  - | Irrelevant
- 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
  - = UserWritten
  - | Inserted
  - | Reflected
  - | CaseSplit
  - | Substitution
- data WithOrigin a = WithOrigin {
  - woOrigin :: !Origin
  - woThing :: a
  }
- class LensOrigin a where
  - getOrigin :: a -> Origin
  - setOrigin :: Origin -> a -> a
  - mapOrigin :: (Origin -> Origin) -> a -> a
- 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 {
  - argInfoHiding :: Hiding
  - argInfoModality :: Modality
  - argInfoOrigin :: Origin
  - argInfoFreeVariables :: FreeVariables
  }
- 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 {
  - argInfo :: ArgInfo
  - unArg :: e
  }
- 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 {
  - domInfo :: ArgInfo
  - domFinite :: !Bool
  - domName :: Maybe RString
  - unDom :: e
  }
- 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
  - lensNamed :: Lens' (Maybe name) a
- 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
  - = ConOSystem
  - | ConOCon
  - | ConORec
  - | ConOSplit
- bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin
- data ProjOrigin
  - = ProjPrefix
  - | ProjPostfix
  - | ProjSystem
- data DataOrRecord
  - = IsData
  - | IsRecord
- data IsInfix
  - = InfixDef
  - | PrefixDef
- data Access
  - = PrivateAccess Origin
  - | PublicAccess
  - | OnlyQualified
- data IsAbstract
  - = AbstractDef
  - | ConcreteDef
- data IsInstance
  - = InstanceDef
  - | NotInstanceDef
- data IsMacro
  - = MacroDef
  - | NotMacroDef
- type Nat = Int
- type Arity = Nat
- data NameId = NameId !Word64 !Word64
- newtype MetaId = MetaId {
  - metaId :: Nat
  }
- newtype Constr a = Constr a
- data PositionInName
  - = Beginning
  - | Middle
  - | End
- data MaybePlaceholder e
  - = Placeholder !PositionInName
  - | NoPlaceholder !(Maybe PositionInName) 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
  - = TerminationCheck
  - | NoTerminationCheck
  - | NonTerminating
  - | Terminating
  - | TerminationMeasure Range m
- type PositivityCheck = Bool
- data UniverseCheck
  - = YesUniverseCheck
  - | NoUniverseCheck

# Delayed

data Delayed Source #

Used to specify whether something should be delayed.

Constructors

Delayed |
NotDelayed |

Instances

Eq Delayed Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Delayed -> Delayed -> Bool Source # (/=) :: Delayed -> Delayed -> Bool Source #
Data Delayed Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Delayed Source #

toConstr :: Delayed -> Constr Source #

dataTypeOf :: Delayed -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Delayed) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Delayed) Source #

gmapT :: (forall b. Data b => b -> b) -> Delayed -> Delayed Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Delayed -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Delayed -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed Source #

Ord Delayed Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: Delayed -> Delayed -> Ordering Source # (<) :: Delayed -> Delayed -> Bool Source # (<=) :: Delayed -> Delayed -> Bool Source # (>) :: Delayed -> Delayed -> Bool Source # (>=) :: Delayed -> Delayed -> Bool Source # max :: Delayed -> Delayed -> Delayed Source # min :: Delayed -> Delayed -> Delayed Source #
Show Delayed Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Delayed -> ShowS Source # show :: Delayed -> String Source # showList :: [Delayed] -> ShowS Source #
KillRange Delayed Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Delayed Source #
EmbPrj Delayed Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Delayed -> S Int32 Source # icod_ :: Delayed -> S Int32 Source # value :: Int32 -> R Delayed Source #

# File

data FileType Source #

Constructors

AgdaFileType |
MdFileType |
RstFileType |
TexFileType |
OrgFileType |

Instances

Eq FileType Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: FileType -> FileType -> Bool Source # (/=) :: FileType -> FileType -> Bool Source #
Data FileType Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FileType Source #

toConstr :: FileType -> Constr Source #

dataTypeOf :: FileType -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FileType) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FileType) Source #

gmapT :: (forall b. Data b => b -> b) -> FileType -> FileType Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FileType -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FileType -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> FileType -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> FileType -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FileType -> m FileType Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FileType -> m FileType Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FileType -> m FileType Source #

Ord FileType Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: FileType -> FileType -> Ordering Source # (<) :: FileType -> FileType -> Bool Source # (<=) :: FileType -> FileType -> Bool Source # (>) :: FileType -> FileType -> Bool Source # (>=) :: FileType -> FileType -> Bool Source # max :: FileType -> FileType -> FileType Source # min :: FileType -> FileType -> FileType Source #
Show FileType Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> FileType -> ShowS Source # show :: FileType -> String Source # showList :: [FileType] -> ShowS Source #
Pretty FileType Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: FileType -> Doc Source # prettyPrec :: Int -> FileType -> Doc Source # prettyList :: [FileType] -> Doc Source #
EmbPrj FileType Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FileType -> S Int32 Source # icod_ :: FileType -> S Int32 Source # value :: Int32 -> R FileType Source #

# Eta-equality

data HasEta Source #

Constructors

NoEta |
YesEta |

Instances

Eq HasEta Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: HasEta -> HasEta -> Bool Source # (/=) :: HasEta -> HasEta -> Bool Source #
Data HasEta Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HasEta Source #

toConstr :: HasEta -> Constr Source #

dataTypeOf :: HasEta -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HasEta) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HasEta) Source #

gmapT :: (forall b. Data b => b -> b) -> HasEta -> HasEta Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HasEta -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HasEta -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> HasEta -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> HasEta -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta Source #

Ord HasEta Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: HasEta -> HasEta -> Ordering Source # (<) :: HasEta -> HasEta -> Bool Source # (<=) :: HasEta -> HasEta -> Bool Source # (>) :: HasEta -> HasEta -> Bool Source # (>=) :: HasEta -> HasEta -> Bool Source # max :: HasEta -> HasEta -> HasEta Source # min :: HasEta -> HasEta -> HasEta Source #
Show HasEta Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> HasEta -> ShowS Source # show :: HasEta -> String Source # showList :: [HasEta] -> ShowS Source #
NFData HasEta Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: HasEta -> () Source #
KillRange HasEta Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT HasEta Source #
HasRange HasEta Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: HasEta -> Range Source #
EmbPrj HasEta Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: HasEta -> S Int32 Source # icod_ :: HasEta -> S Int32 Source # value :: Int32 -> R HasEta Source #

# Induction

data Induction Source #

Constructors

Inductive |
CoInductive |

Instances

Eq Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Induction -> Induction -> Bool Source # (/=) :: Induction -> Induction -> Bool Source #
Data Induction Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Induction Source #

toConstr :: Induction -> Constr Source #

dataTypeOf :: Induction -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Induction) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Induction) Source #

gmapT :: (forall b. Data b => b -> b) -> Induction -> Induction Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Induction -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Induction -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Induction -> m Induction Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction Source #

Ord Induction Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Induction -> Induction -> Ordering Source #

(<) :: Induction -> Induction -> Bool Source #

(<=) :: Induction -> Induction -> Bool Source #

(>) :: Induction -> Induction -> Bool Source #

(>=) :: Induction -> Induction -> Bool Source #

max :: Induction -> Induction -> Induction Source #

min :: Induction -> Induction -> Induction Source #

Show Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Induction -> ShowS Source # show :: Induction -> String Source # showList :: [Induction] -> ShowS Source #
NFData Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Induction -> () Source #
Pretty Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Induction -> Doc Source # prettyPrec :: Int -> Induction -> Doc Source # prettyList :: [Induction] -> Doc Source #
KillRange Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Induction Source #
HasRange Induction Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Induction -> Range Source #
EmbPrj Induction Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Induction -> S Int32 Source # icod_ :: Induction -> S Int32 Source # value :: Int32 -> R Induction Source #

# Hiding

data Overlappable Source #

Constructors

YesOverlap |
NoOverlap |

Instances

Eq Overlappable Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Overlappable -> Overlappable -> Bool Source # (/=) :: Overlappable -> Overlappable -> Bool Source #
Data Overlappable Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Overlappable Source #

toConstr :: Overlappable -> Constr Source #

dataTypeOf :: Overlappable -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Overlappable) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Overlappable) Source #

gmapT :: (forall b. Data b => b -> b) -> Overlappable -> Overlappable Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Overlappable -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Overlappable -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Overlappable -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Overlappable -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable Source #

Ord Overlappable Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Overlappable -> Overlappable -> Ordering Source #

(<) :: Overlappable -> Overlappable -> Bool Source #

(<=) :: Overlappable -> Overlappable -> Bool Source #

(>) :: Overlappable -> Overlappable -> Bool Source #

(>=) :: Overlappable -> Overlappable -> Bool Source #

max :: Overlappable -> Overlappable -> Overlappable Source #

min :: Overlappable -> Overlappable -> Overlappable Source #

Show Overlappable Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Overlappable -> ShowS Source # show :: Overlappable -> String Source # showList :: [Overlappable] -> ShowS Source #
Semigroup Overlappable Source # | Just for the `Hiding` instance. Should never combine different overlapping.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Overlappable -> Overlappable -> Overlappable Source # sconcat :: NonEmpty Overlappable -> Overlappable Source # stimes :: Integral b => b -> Overlappable -> Overlappable Source #
Monoid Overlappable Source # |
Instance details Defined in Agda.Syntax.Common Methods mempty :: Overlappable Source # mappend :: Overlappable -> Overlappable -> Overlappable Source # mconcat :: [Overlappable] -> Overlappable Source #
NFData Overlappable Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Overlappable -> () Source #

data Hiding Source #

Constructors

Hidden |
Instance Overlappable |
NotHidden |

Instances

Eq Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Hiding -> Hiding -> Bool Source # (/=) :: Hiding -> Hiding -> Bool Source #
Data Hiding Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Hiding Source #

toConstr :: Hiding -> Constr Source #

dataTypeOf :: Hiding -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Hiding) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Hiding) Source #

gmapT :: (forall b. Data b => b -> b) -> Hiding -> Hiding Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Hiding -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Hiding -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding Source #

Ord Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: Hiding -> Hiding -> Ordering Source # (<) :: Hiding -> Hiding -> Bool Source # (<=) :: Hiding -> Hiding -> Bool Source # (>) :: Hiding -> Hiding -> Bool Source # (>=) :: Hiding -> Hiding -> Bool Source # max :: Hiding -> Hiding -> Hiding Source # min :: Hiding -> Hiding -> Hiding Source #
Show Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Hiding -> ShowS Source # show :: Hiding -> String Source # showList :: [Hiding] -> ShowS Source #
Semigroup Hiding Source # | `Hiding` is an idempotent partial monoid, with unit `NotHidden`. `Instance` and `NotHidden` are incompatible.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Hiding -> Hiding -> Hiding Source # sconcat :: NonEmpty Hiding -> Hiding Source # stimes :: Integral b => b -> Hiding -> Hiding Source #
Monoid Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods mempty :: Hiding Source # mappend :: Hiding -> Hiding -> Hiding Source # mconcat :: [Hiding] -> Hiding Source #
NFData Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Hiding -> () Source #
Pretty Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Hiding -> Doc Source # prettyPrec :: Int -> Hiding -> Doc Source # prettyList :: [Hiding] -> Doc Source #
KillRange Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Hiding Source #
LensHiding Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods getHiding :: Hiding -> Hiding Source # setHiding :: Hiding -> Hiding -> Hiding Source # mapHiding :: (Hiding -> Hiding) -> Hiding -> Hiding Source #
EmbPrj Hiding Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Hiding -> S Int32 Source # icod_ :: Hiding -> S Int32 Source # value :: Int32 -> R Hiding Source #
ChooseFlex Hiding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Hiding -> Hiding -> FlexChoice Source #
Unquote Hiding Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Hiding Source #
Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg a -> TOM (Hiding, b) Source #

data WithHiding a Source #

Decorating something with `Hiding` information.

Constructors

WithHiding |

Fields

- whHiding :: !Hiding
- whThing :: a

Instances

Functor WithHiding Source # |
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> WithHiding a -> WithHiding b Source # (<$) :: a -> WithHiding b -> WithHiding a Source #
Applicative WithHiding Source # |
Instance details Defined in Agda.Syntax.Common Methods pure :: a -> WithHiding a Source # (<*>) :: WithHiding (a -> b) -> WithHiding a -> WithHiding b Source # liftA2 :: (a -> b -> c) -> WithHiding a -> WithHiding b -> WithHiding c Source # (*>) :: WithHiding a -> WithHiding b -> WithHiding b Source # (<*) :: WithHiding a -> WithHiding b -> WithHiding a Source #
Foldable WithHiding Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => WithHiding m -> m Source #

foldMap :: Monoid m => (a -> m) -> WithHiding a -> m Source #

foldr :: (a -> b -> b) -> b -> WithHiding a -> b Source #

foldr' :: (a -> b -> b) -> b -> WithHiding a -> b Source #

foldl :: (b -> a -> b) -> b -> WithHiding a -> b Source #

foldl' :: (b -> a -> b) -> b -> WithHiding a -> b Source #

foldr1 :: (a -> a -> a) -> WithHiding a -> a Source #

foldl1 :: (a -> a -> a) -> WithHiding a -> a Source #

toList :: WithHiding a -> [a] Source #

null :: WithHiding a -> Bool Source #

length :: WithHiding a -> Int Source #

elem :: Eq a => a -> WithHiding a -> Bool Source #

maximum :: Ord a => WithHiding a -> a Source #

minimum :: Ord a => WithHiding a -> a Source #

sum :: Num a => WithHiding a -> a Source #

product :: Num a => WithHiding a -> a Source #

Traversable WithHiding Source # |
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> WithHiding a -> f (WithHiding b) Source # sequenceA :: Applicative f => WithHiding (f a) -> f (WithHiding a) Source # mapM :: Monad m => (a -> m b) -> WithHiding a -> m (WithHiding b) Source # sequence :: Monad m => WithHiding (m a) -> m (WithHiding a) Source #
Decoration WithHiding Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> WithHiding a -> m (WithHiding b) Source # distributeF :: Functor m => WithHiding (m a) -> m (WithHiding a) Source #
Eq a => Eq (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: WithHiding a -> WithHiding a -> Bool Source # (/=) :: WithHiding a -> WithHiding a -> Bool Source #
Data a => Data (WithHiding a) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WithHiding a -> c (WithHiding a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WithHiding a) Source #

toConstr :: WithHiding a -> Constr Source #

dataTypeOf :: WithHiding a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WithHiding a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WithHiding a)) Source #

gmapT :: (forall b. Data b => b -> b) -> WithHiding a -> WithHiding a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithHiding a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithHiding a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> WithHiding a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> WithHiding a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithHiding a -> m (WithHiding a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithHiding a -> m (WithHiding a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithHiding a -> m (WithHiding a) Source #

Ord a => Ord (WithHiding a) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: WithHiding a -> WithHiding a -> Ordering Source #

(<) :: WithHiding a -> WithHiding a -> Bool Source #

(<=) :: WithHiding a -> WithHiding a -> Bool Source #

(>) :: WithHiding a -> WithHiding a -> Bool Source #

(>=) :: WithHiding a -> WithHiding a -> Bool Source #

max :: WithHiding a -> WithHiding a -> WithHiding a Source #

min :: WithHiding a -> WithHiding a -> WithHiding a Source #

Show a => Show (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> WithHiding a -> ShowS Source # show :: WithHiding a -> String Source # showList :: [WithHiding a] -> ShowS Source #
NFData a => NFData (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: WithHiding a -> () Source #
Pretty a => Pretty (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WithHiding a -> Doc Source # prettyPrec :: Int -> WithHiding a -> Doc Source # prettyList :: [WithHiding a] -> Doc Source #
KillRange a => KillRange (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (WithHiding a) Source #
SetRange a => SetRange (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> WithHiding a -> WithHiding a Source #
HasRange a => HasRange (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: WithHiding a -> Range Source #
LensHiding (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getHiding :: WithHiding a -> Hiding Source # setHiding :: Hiding -> WithHiding a -> WithHiding a Source # mapHiding :: (Hiding -> Hiding) -> WithHiding a -> WithHiding a Source #
EmbPrj a => EmbPrj (WithHiding a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithHiding a -> S Int32 Source # icod_ :: WithHiding a -> S Int32 Source # value :: Int32 -> R (WithHiding a) Source #
PrettyTCM a => PrettyTCM (WithHiding a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: WithHiding a -> TCM Doc Source #
ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: WithHiding a -> AbsToCon (WithHiding c) Source # bindToConcrete :: WithHiding a -> (WithHiding c -> AbsToCon b) -> AbsToCon b Source #
ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: WithHiding c -> ScopeM (WithHiding a) Source #
AddContext ([WithHiding Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #

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

getHiding

Methods

getHiding :: a -> Hiding Source #

setHiding :: Hiding -> a -> a Source #

mapHiding :: (Hiding -> Hiding) -> a -> a Source #

Instances

LensHiding ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getHiding :: ArgInfo -> Hiding Source # setHiding :: Hiding -> ArgInfo -> ArgInfo Source # mapHiding :: (Hiding -> Hiding) -> ArgInfo -> ArgInfo Source #
LensHiding Hiding Source # |
Instance details Defined in Agda.Syntax.Common Methods getHiding :: Hiding -> Hiding Source # setHiding :: Hiding -> Hiding -> Hiding Source # mapHiding :: (Hiding -> Hiding) -> Hiding -> Hiding Source #
LensHiding TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source #
LensHiding LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
LensHiding TypedBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source #
LensHiding LamBinding Source # |
Instance details Defined in Agda.Syntax.Abstract Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
LensHiding (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getHiding :: Dom e -> Hiding Source # setHiding :: Hiding -> Dom e -> Dom e Source # mapHiding :: (Hiding -> Hiding) -> Dom e -> Dom e Source #
LensHiding (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getHiding :: Arg e -> Hiding Source # setHiding :: Hiding -> Arg e -> Arg e Source # mapHiding :: (Hiding -> Hiding) -> Arg e -> Arg e Source #
LensHiding (WithHiding a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getHiding :: WithHiding a -> Hiding Source # setHiding :: Hiding -> WithHiding a -> WithHiding a Source # mapHiding :: (Hiding -> Hiding) -> WithHiding a -> WithHiding a Source #
LensHiding (FlexibleVar a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getHiding :: FlexibleVar a -> Hiding Source # setHiding :: Hiding -> FlexibleVar a -> FlexibleVar a Source # mapHiding :: (Hiding -> Hiding) -> FlexibleVar a -> FlexibleVar a Source #

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 #

`Instance` and `Hidden` arguments are `notVisible`.

hidden :: 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

data Modality Source #

We have a tuple of modalities, which might not be fully orthogonal. For instance, irrelevant stuff is also run-time irrelevant.

Constructors

Modality |

Fields

- modRelevance :: Relevance

  Legacy irrelevance. See Pfenning, LiCS 2001; AbelVezzosiWinterhalter, ICFP 2017.

- modQuantity :: Quantity

  Cardinality / runtime erasure. See Conor McBride, I got plenty o' nutting, Wadlerfest 2016. See Bob Atkey, Syntax and Semantics of Quantitative Type Theory, LiCS 2018.

Instances

Eq Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Modality -> Modality -> Bool Source # (/=) :: Modality -> Modality -> Bool Source #
Data Modality Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Modality Source #

toConstr :: Modality -> Constr Source #

dataTypeOf :: Modality -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Modality) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Modality) Source #

gmapT :: (forall b. Data b => b -> b) -> Modality -> Modality Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Modality -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Modality -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Modality -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Modality -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Modality -> m Modality Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Modality -> m Modality Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Modality -> m Modality Source #

Ord Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: Modality -> Modality -> Ordering Source # (<) :: Modality -> Modality -> Bool Source # (<=) :: Modality -> Modality -> Bool Source # (>) :: Modality -> Modality -> Bool Source # (>=) :: Modality -> Modality -> Bool Source # max :: Modality -> Modality -> Modality Source # min :: Modality -> Modality -> Modality Source #
Show Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Modality -> ShowS Source # show :: Modality -> String Source # showList :: [Modality] -> ShowS Source #
Generic Modality Source # |
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Modality :: Type -> Type Source # Methods from :: Modality -> Rep Modality x Source # to :: Rep Modality x -> Modality Source #
Semigroup Modality Source # | Pointwise composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Modality -> Modality -> Modality Source # sconcat :: NonEmpty Modality -> Modality Source # stimes :: Integral b => b -> Modality -> Modality Source #
Monoid Modality Source # | Pointwise unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: Modality Source # mappend :: Modality -> Modality -> Modality Source # mconcat :: [Modality] -> Modality Source #
NFData Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Modality -> () Source #
PartialOrd Modality Source # | Dominance ordering.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Modality Source #
LeftClosedPOMonoid Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: Modality -> Modality -> Modality Source #
POMonoid Modality Source # |
Instance details Defined in Agda.Syntax.Common
POSemigroup Modality Source # |
Instance details Defined in Agda.Syntax.Common
KillRange Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Modality Source #
LensRelevance Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods getRelevance :: Modality -> Relevance Source # setRelevance :: Relevance -> Modality -> Modality Source # mapRelevance :: (Relevance -> Relevance) -> Modality -> Modality Source #
LensQuantity Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods getQuantity :: Modality -> Quantity Source # setQuantity :: Quantity -> Modality -> Modality Source # mapQuantity :: (Quantity -> Quantity) -> Modality -> Modality Source #
LensModality Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods getModality :: Modality -> Modality Source # setModality :: Modality -> Modality -> Modality Source # mapModality :: (Modality -> Modality) -> Modality -> Modality Source #
EmbPrj Modality Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Modality -> S Int32 Source # icod_ :: Modality -> S Int32 Source # value :: Int32 -> R Modality Source #
Unquote Modality Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Modality Source #
type Rep Modality Source # |

Instance details

Defined in Agda.Syntax.Common

type Rep Modality = D1 (MetaData "Modality" "Agda.Syntax.Common" "Agda-2.6.0.1-1X7fHcR3xPHzuc9vp1IMb" False) (C1 (MetaCons "Modality" PrefixI True) (S1 (MetaSel (Just "modRelevance") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Relevance) :*: S1 (MetaSel (Just "modQuantity") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Quantity)))

defaultModality :: Modality Source #

moreUsableModality :: Modality -> Modality -> Bool Source #

`m `moreUsableModality` m'` means that an `m` can be used where ever an `m'` is required.

usableModality :: LensModality a => a -> Bool Source #

composeModality :: Modality -> Modality -> Modality 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.

lModRelevance :: Lens' Relevance Modality Source #

lModQuantity :: Lens' Quantity Modality Source #

class LensModality a where Source #

Minimal complete definition

getModality

Methods

getModality :: a -> Modality Source #

setModality :: Modality -> a -> a Source #

mapModality :: (Modality -> Modality) -> a -> a Source #

Instances

LensModality ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getModality :: ArgInfo -> Modality Source # setModality :: Modality -> ArgInfo -> ArgInfo Source # mapModality :: (Modality -> Modality) -> ArgInfo -> ArgInfo Source #
LensModality Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods getModality :: Modality -> Modality Source # setModality :: Modality -> Modality -> Modality Source # mapModality :: (Modality -> Modality) -> Modality -> Modality Source #
LensModality (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getModality :: Dom e -> Modality Source # setModality :: Modality -> Dom e -> Dom e Source # mapModality :: (Modality -> Modality) -> Dom e -> Dom e Source #
LensModality (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getModality :: Arg e -> Modality Source # setModality :: Modality -> Arg e -> Arg e Source # mapModality :: (Modality -> Modality) -> Arg e -> Arg e Source #

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

data Quantity Source #

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 `{0}`, erased at runtime.
Quantity1 | Linear use `{1}` (could be updated destructively). Mostly TODO (needs postponable constraints between quantities to compute uses).
Quantityω | Unrestricted use `ℕ`.

Instances

Bounded Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods minBound :: Quantity Source # maxBound :: Quantity Source #
Enum Quantity Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: Quantity -> Quantity Source #

pred :: Quantity -> Quantity Source #

toEnum :: Int -> Quantity Source #

fromEnum :: Quantity -> Int Source #

enumFrom :: Quantity -> [Quantity] Source #

enumFromThen :: Quantity -> Quantity -> [Quantity] Source #

enumFromTo :: Quantity -> Quantity -> [Quantity] Source #

enumFromThenTo :: Quantity -> Quantity -> Quantity -> [Quantity] Source #

Eq Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Quantity -> Quantity -> Bool Source # (/=) :: Quantity -> Quantity -> Bool Source #
Data Quantity Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quantity Source #

toConstr :: Quantity -> Constr Source #

dataTypeOf :: Quantity -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quantity) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantity) Source #

gmapT :: (forall b. Data b => b -> b) -> Quantity -> Quantity Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Quantity -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Quantity -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity Source #

Ord Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: Quantity -> Quantity -> Ordering Source # (<) :: Quantity -> Quantity -> Bool Source # (<=) :: Quantity -> Quantity -> Bool Source # (>) :: Quantity -> Quantity -> Bool Source # (>=) :: Quantity -> Quantity -> Bool Source # max :: Quantity -> Quantity -> Quantity Source # min :: Quantity -> Quantity -> Quantity Source #
Show Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Quantity -> ShowS Source # show :: Quantity -> String Source # showList :: [Quantity] -> ShowS Source #
Generic Quantity Source # |
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Quantity :: Type -> Type Source # Methods from :: Quantity -> Rep Quantity x Source # to :: Rep Quantity x -> Quantity Source #
Semigroup Quantity Source # | Composition of quantities (multiplication). `Quantity0` is dominant. `Quantity1` is neutral.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Quantity -> Quantity -> Quantity Source # sconcat :: NonEmpty Quantity -> Quantity Source # stimes :: Integral b => b -> Quantity -> Quantity Source #
Monoid Quantity Source # | In the absense of finite quantities besides 0, ω is the unit. Otherwise, 1 is the unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: Quantity Source # mappend :: Quantity -> Quantity -> Quantity Source # mconcat :: [Quantity] -> Quantity Source #
NFData Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Quantity -> () Source #
PartialOrd Quantity Source # | Note that the order is `ω ≤ 0,1`, more options is smaller.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Quantity Source #
LeftClosedPOMonoid Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: Quantity -> Quantity -> Quantity Source #
POMonoid Quantity Source # |
Instance details Defined in Agda.Syntax.Common
POSemigroup Quantity Source # |
Instance details Defined in Agda.Syntax.Common
KillRange Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Quantity Source #
LensQuantity Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods getQuantity :: Quantity -> Quantity Source # setQuantity :: Quantity -> Quantity -> Quantity Source # mapQuantity :: (Quantity -> Quantity) -> Quantity -> Quantity Source #
EmbPrj Quantity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Quantity -> S Int32 Source # icod_ :: Quantity -> S Int32 Source # value :: Int32 -> R Quantity Source #
type Rep Quantity Source # |
Instance details Defined in Agda.Syntax.Common type Rep Quantity = D1 (MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.0.1-1X7fHcR3xPHzuc9vp1IMb" 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)))

defaultQuantity :: Quantity Source #

moreQuantity :: Quantity -> Quantity -> Bool Source #

`m `moreUsableQuantity` m'` means that an `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.

composeQuantity :: Quantity -> Quantity -> Quantity Source #

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

getQuantity

Methods

getQuantity :: a -> Quantity Source #

setQuantity :: Quantity -> a -> a Source #

mapQuantity :: (Quantity -> Quantity) -> a -> a Source #

Instances

LensQuantity ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getQuantity :: ArgInfo -> Quantity Source # setQuantity :: Quantity -> ArgInfo -> ArgInfo Source # mapQuantity :: (Quantity -> Quantity) -> ArgInfo -> ArgInfo Source #
LensQuantity Quantity Source # |
Instance details Defined in Agda.Syntax.Common Methods getQuantity :: Quantity -> Quantity Source # setQuantity :: Quantity -> Quantity -> Quantity Source # mapQuantity :: (Quantity -> Quantity) -> Quantity -> Quantity Source #
LensQuantity Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods getQuantity :: Modality -> Quantity Source # setQuantity :: Quantity -> Modality -> Modality Source # mapQuantity :: (Quantity -> Quantity) -> Modality -> Modality Source #
LensQuantity (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getQuantity :: Dom e -> Quantity Source # setQuantity :: Quantity -> Dom e -> Dom e Source # mapQuantity :: (Quantity -> Quantity) -> Dom e -> Dom e Source #
LensQuantity (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getQuantity :: Arg e -> Quantity Source # setQuantity :: Quantity -> Arg e -> Arg e Source # mapQuantity :: (Quantity -> Quantity) -> Arg e -> Arg e Source #

# Relevance

data Relevance Source #

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 # |
Instance details Defined in Agda.Syntax.Common Methods minBound :: Relevance Source # maxBound :: Relevance Source #
Enum Relevance Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: Relevance -> Relevance Source #

pred :: Relevance -> Relevance Source #

toEnum :: Int -> Relevance Source #

fromEnum :: Relevance -> Int Source #

enumFrom :: Relevance -> [Relevance] Source #

enumFromThen :: Relevance -> Relevance -> [Relevance] Source #

enumFromTo :: Relevance -> Relevance -> [Relevance] Source #

enumFromThenTo :: Relevance -> Relevance -> Relevance -> [Relevance] Source #

Eq Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Relevance -> Relevance -> Bool Source # (/=) :: Relevance -> Relevance -> Bool Source #
Data Relevance Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Relevance Source #

toConstr :: Relevance -> Constr Source #

dataTypeOf :: Relevance -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Relevance) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Relevance) Source #

gmapT :: (forall b. Data b => b -> b) -> Relevance -> Relevance Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Relevance -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Relevance -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Relevance -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Relevance -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance Source #

Ord Relevance Source # | More relevant is smaller.

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Relevance -> Relevance -> Ordering Source #

(<) :: Relevance -> Relevance -> Bool Source #

(<=) :: Relevance -> Relevance -> Bool Source #

(>) :: Relevance -> Relevance -> Bool Source #

(>=) :: Relevance -> Relevance -> Bool Source #

max :: Relevance -> Relevance -> Relevance Source #

min :: Relevance -> Relevance -> Relevance Source #

Show Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Relevance -> ShowS Source # show :: Relevance -> String Source # showList :: [Relevance] -> ShowS Source #
Generic Relevance Source # |
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Relevance :: Type -> Type Source # Methods from :: Relevance -> Rep Relevance x Source # to :: Rep Relevance x -> Relevance Source #
Semigroup Relevance Source # | `Relevance` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Relevance -> Relevance -> Relevance Source # sconcat :: NonEmpty Relevance -> Relevance Source # stimes :: Integral b => b -> Relevance -> Relevance Source #
Monoid Relevance Source # | `Relevant` is the unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: Relevance Source # mappend :: Relevance -> Relevance -> Relevance Source # mconcat :: [Relevance] -> Relevance Source #
NFData Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Relevance -> () Source #
PartialOrd Relevance Source # | More relevant is smaller.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Relevance Source #
LeftClosedPOMonoid Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: Relevance -> Relevance -> Relevance Source #
POMonoid Relevance Source # |
Instance details Defined in Agda.Syntax.Common
POSemigroup Relevance Source # |
Instance details Defined in Agda.Syntax.Common
Pretty Relevance Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Relevance -> Doc Source # prettyPrec :: Int -> Relevance -> Doc Source # prettyList :: [Relevance] -> Doc Source #
KillRange Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Relevance Source #
LensRelevance Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods getRelevance :: Relevance -> Relevance Source # setRelevance :: Relevance -> Relevance -> Relevance Source # mapRelevance :: (Relevance -> Relevance) -> Relevance -> Relevance Source #
EmbPrj Relevance Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Relevance -> S Int32 Source # icod_ :: Relevance -> S Int32 Source # value :: Int32 -> R Relevance Source #
PrettyTCM Relevance Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Relevance -> TCM Doc Source #
Unquote Relevance Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Relevance Source #
type Rep Relevance Source # |
Instance details Defined in Agda.Syntax.Common type Rep Relevance = D1 (MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.6.0.1-1X7fHcR3xPHzuc9vp1IMb" 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 #

defaultRelevance :: 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

getRelevance

Methods

getRelevance :: a -> Relevance Source #

setRelevance :: Relevance -> a -> a Source #

mapRelevance :: (Relevance -> Relevance) -> a -> a Source #

Instances

LensRelevance ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getRelevance :: ArgInfo -> Relevance Source # setRelevance :: Relevance -> ArgInfo -> ArgInfo Source # mapRelevance :: (Relevance -> Relevance) -> ArgInfo -> ArgInfo Source #
LensRelevance Relevance Source # |
Instance details Defined in Agda.Syntax.Common Methods getRelevance :: Relevance -> Relevance Source # setRelevance :: Relevance -> Relevance -> Relevance Source # mapRelevance :: (Relevance -> Relevance) -> Relevance -> Relevance Source #
LensRelevance Modality Source # |
Instance details Defined in Agda.Syntax.Common Methods getRelevance :: Modality -> Relevance Source # setRelevance :: Relevance -> Modality -> Modality Source # mapRelevance :: (Relevance -> Relevance) -> Modality -> Modality Source #
LensRelevance TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRelevance :: TypedBinding -> Relevance Source # setRelevance :: Relevance -> TypedBinding -> TypedBinding Source # mapRelevance :: (Relevance -> Relevance) -> TypedBinding -> TypedBinding Source #
LensRelevance VarOcc Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getRelevance :: VarOcc -> Relevance Source # setRelevance :: Relevance -> VarOcc -> VarOcc Source # mapRelevance :: (Relevance -> Relevance) -> VarOcc -> VarOcc Source #
LensRelevance (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRelevance :: Dom e -> Relevance Source # setRelevance :: Relevance -> Dom e -> Dom e Source # mapRelevance :: (Relevance -> Relevance) -> Dom e -> Dom e Source #
LensRelevance (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRelevance :: Arg e -> Relevance Source # setRelevance :: Relevance -> Arg e -> Arg e Source # mapRelevance :: (Relevance -> Relevance) -> Arg e -> Arg e Source #

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)

data Origin Source #

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 # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Origin -> Origin -> Bool Source # (/=) :: Origin -> Origin -> Bool Source #
Data Origin Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Origin Source #

toConstr :: Origin -> Constr Source #

dataTypeOf :: Origin -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Origin) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Origin) Source #

gmapT :: (forall b. Data b => b -> b) -> Origin -> Origin Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Origin -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Origin -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Origin -> m Origin Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin Source #

Ord Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: Origin -> Origin -> Ordering Source # (<) :: Origin -> Origin -> Bool Source # (<=) :: Origin -> Origin -> Bool Source # (>) :: Origin -> Origin -> Bool Source # (>=) :: Origin -> Origin -> Bool Source # max :: Origin -> Origin -> Origin Source # min :: Origin -> Origin -> Origin Source #
Show Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Origin -> ShowS Source # show :: Origin -> String Source # showList :: [Origin] -> ShowS Source #
NFData Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Origin -> () Source #
KillRange Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Origin Source #
LensOrigin Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods getOrigin :: Origin -> Origin Source # setOrigin :: Origin -> Origin -> Origin Source # mapOrigin :: (Origin -> Origin) -> Origin -> Origin Source #
EmbPrj Origin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Origin -> S Int32 Source # icod_ :: Origin -> S Int32 Source # value :: Int32 -> R Origin Source #
ChooseFlex Origin Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Origin -> Origin -> FlexChoice Source #

data WithOrigin a Source #

Decorating something with `Origin` information.

Constructors

WithOrigin |

Fields

- woOrigin :: !Origin
- woThing :: a

Instances

Functor WithOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> WithOrigin a -> WithOrigin b Source # (<$) :: a -> WithOrigin b -> WithOrigin a Source #
Foldable WithOrigin Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => WithOrigin m -> m Source #

foldMap :: Monoid m => (a -> m) -> WithOrigin a -> m Source #

foldr :: (a -> b -> b) -> b -> WithOrigin a -> b Source #

foldr' :: (a -> b -> b) -> b -> WithOrigin a -> b Source #

foldl :: (b -> a -> b) -> b -> WithOrigin a -> b Source #

foldl' :: (b -> a -> b) -> b -> WithOrigin a -> b Source #

foldr1 :: (a -> a -> a) -> WithOrigin a -> a Source #

foldl1 :: (a -> a -> a) -> WithOrigin a -> a Source #

toList :: WithOrigin a -> [a] Source #

null :: WithOrigin a -> Bool Source #

length :: WithOrigin a -> Int Source #

elem :: Eq a => a -> WithOrigin a -> Bool Source #

maximum :: Ord a => WithOrigin a -> a Source #

minimum :: Ord a => WithOrigin a -> a Source #

sum :: Num a => WithOrigin a -> a Source #

product :: Num a => WithOrigin a -> a Source #

Traversable WithOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> WithOrigin a -> f (WithOrigin b) Source # sequenceA :: Applicative f => WithOrigin (f a) -> f (WithOrigin a) Source # mapM :: Monad m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) Source # sequence :: Monad m => WithOrigin (m a) -> m (WithOrigin a) Source #
Decoration WithOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) Source # distributeF :: Functor m => WithOrigin (m a) -> m (WithOrigin a) Source #
Eq a => Eq (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: WithOrigin a -> WithOrigin a -> Bool Source # (/=) :: WithOrigin a -> WithOrigin a -> Bool Source #
Data a => Data (WithOrigin a) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WithOrigin a -> c (WithOrigin a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WithOrigin a) Source #

toConstr :: WithOrigin a -> Constr Source #

dataTypeOf :: WithOrigin a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WithOrigin a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WithOrigin a)) Source #

gmapT :: (forall b. Data b => b -> b) -> WithOrigin a -> WithOrigin a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithOrigin a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithOrigin a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> WithOrigin a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> WithOrigin a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a) Source #

Ord a => Ord (WithOrigin a) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: WithOrigin a -> WithOrigin a -> Ordering Source #

(<) :: WithOrigin a -> WithOrigin a -> Bool Source #

(<=) :: WithOrigin a -> WithOrigin a -> Bool Source #

(>) :: WithOrigin a -> WithOrigin a -> Bool Source #

(>=) :: WithOrigin a -> WithOrigin a -> Bool Source #

max :: WithOrigin a -> WithOrigin a -> WithOrigin a Source #

min :: WithOrigin a -> WithOrigin a -> WithOrigin a Source #

Show a => Show (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> WithOrigin a -> ShowS Source # show :: WithOrigin a -> String Source # showList :: [WithOrigin a] -> ShowS Source #
NFData a => NFData (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: WithOrigin a -> () Source #
KillRange a => KillRange (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (WithOrigin a) Source #
SetRange a => SetRange (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> WithOrigin a -> WithOrigin a Source #
HasRange a => HasRange (WithOrigin a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: WithOrigin a -> Range Source #
LensOrigin (WithOrigin a) Source # |
Instance details 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 #

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

getOrigin

Methods

getOrigin :: a -> Origin Source #

setOrigin :: Origin -> a -> a Source #

mapOrigin :: (Origin -> Origin) -> a -> a Source #

Instances

LensOrigin ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getOrigin :: ArgInfo -> Origin Source # setOrigin :: Origin -> ArgInfo -> ArgInfo Source # mapOrigin :: (Origin -> Origin) -> ArgInfo -> ArgInfo Source #
LensOrigin Origin Source # |
Instance details Defined in Agda.Syntax.Common Methods getOrigin :: Origin -> Origin Source # setOrigin :: Origin -> Origin -> Origin Source # mapOrigin :: (Origin -> Origin) -> Origin -> Origin Source #
LensOrigin AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getOrigin :: AppInfo -> Origin Source # setOrigin :: Origin -> AppInfo -> AppInfo Source # mapOrigin :: (Origin -> Origin) -> AppInfo -> AppInfo Source #
LensOrigin (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getOrigin :: Dom e -> Origin Source # setOrigin :: Origin -> Dom e -> Dom e Source # mapOrigin :: (Origin -> Origin) -> Dom e -> Dom e Source #
LensOrigin (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getOrigin :: Arg e -> Origin Source # setOrigin :: Origin -> Arg e -> Arg e Source # mapOrigin :: (Origin -> Origin) -> Arg e -> Arg e Source #
LensOrigin (WithOrigin a) Source # |
Instance details 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 `Proj`, use with care. `Proj`s are always assumed to be `UserWritten`, since they have no `ArgInfo`. Same for IApply
Instance details Defined in Agda.Syntax.Internal Methods getOrigin :: Elim' a -> Origin Source # setOrigin :: Origin -> Elim' a -> Elim' a Source # mapOrigin :: (Origin -> Origin) -> Elim' a -> Elim' a Source #
LensOrigin (FlexibleVar a) Source # |
Instance details 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

Eq FreeVariables Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: FreeVariables -> FreeVariables -> Bool Source # (/=) :: FreeVariables -> FreeVariables -> Bool Source #
Data FreeVariables Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FreeVariables -> c FreeVariables Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FreeVariables Source #

toConstr :: FreeVariables -> Constr Source #

dataTypeOf :: FreeVariables -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FreeVariables) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FreeVariables) Source #

gmapT :: (forall b. Data b => b -> b) -> FreeVariables -> FreeVariables Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FreeVariables -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FreeVariables -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> FreeVariables -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> FreeVariables -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FreeVariables -> m FreeVariables Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FreeVariables -> m FreeVariables Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FreeVariables -> m FreeVariables Source #

Ord FreeVariables Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: FreeVariables -> FreeVariables -> Ordering Source #

(<) :: FreeVariables -> FreeVariables -> Bool Source #

(<=) :: FreeVariables -> FreeVariables -> Bool Source #

(>) :: FreeVariables -> FreeVariables -> Bool Source #

(>=) :: FreeVariables -> FreeVariables -> Bool Source #

max :: FreeVariables -> FreeVariables -> FreeVariables Source #

min :: FreeVariables -> FreeVariables -> FreeVariables Source #

Show FreeVariables Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> FreeVariables -> ShowS Source # show :: FreeVariables -> String Source # showList :: [FreeVariables] -> ShowS Source #
Semigroup FreeVariables Source # |
Instance details Defined in Agda.Syntax.Common Methods (<>) :: FreeVariables -> FreeVariables -> FreeVariables Source # sconcat :: NonEmpty FreeVariables -> FreeVariables Source # stimes :: Integral b => b -> FreeVariables -> FreeVariables Source #
Monoid FreeVariables Source # |
Instance details Defined in Agda.Syntax.Common Methods mempty :: FreeVariables Source # mappend :: FreeVariables -> FreeVariables -> FreeVariables Source # mconcat :: [FreeVariables] -> FreeVariables Source #
NFData FreeVariables Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: FreeVariables -> () Source #
LensFreeVariables FreeVariables Source # |
Instance details Defined in Agda.Syntax.Common Methods getFreeVariables :: FreeVariables -> FreeVariables Source # setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables Source #
EmbPrj FreeVariables Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FreeVariables -> S Int32 Source # icod_ :: FreeVariables -> S Int32 Source # value :: Int32 -> R FreeVariables Source #

unknownFreeVariables :: FreeVariables Source #

noFreeVariables :: FreeVariables Source #

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

getFreeVariables

Methods

getFreeVariables :: a -> FreeVariables Source #

setFreeVariables :: FreeVariables -> a -> a Source #

mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a Source #

Instances

LensFreeVariables ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getFreeVariables :: ArgInfo -> FreeVariables Source # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo Source #
LensFreeVariables FreeVariables Source # |
Instance details Defined in Agda.Syntax.Common Methods getFreeVariables :: FreeVariables -> FreeVariables Source # setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables Source #
LensFreeVariables (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getFreeVariables :: Dom e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Dom e -> Dom e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom e -> Dom e Source #
LensFreeVariables (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getFreeVariables :: Arg e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Arg e -> Arg e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e Source #

hasNoFreeVariables :: LensFreeVariables a => a -> Bool Source #

# Argument decoration

data ArgInfo Source #

A function argument can be hidden and/or irrelevant.

Constructors

ArgInfo |

Fields

- argInfoHiding :: Hiding
- argInfoModality :: Modality
- argInfoOrigin :: Origin
- argInfoFreeVariables :: FreeVariables

Instances

Eq ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: ArgInfo -> ArgInfo -> Bool Source # (/=) :: ArgInfo -> ArgInfo -> Bool Source #
Data ArgInfo Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ArgInfo Source #

toConstr :: ArgInfo -> Constr Source #

dataTypeOf :: ArgInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ArgInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> ArgInfo -> ArgInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArgInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArgInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ArgInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ArgInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo Source #

Ord ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: ArgInfo -> ArgInfo -> Ordering Source # (<) :: ArgInfo -> ArgInfo -> Bool Source # (<=) :: ArgInfo -> ArgInfo -> Bool Source # (>) :: ArgInfo -> ArgInfo -> Bool Source # (>=) :: ArgInfo -> ArgInfo -> Bool Source # max :: ArgInfo -> ArgInfo -> ArgInfo Source # min :: ArgInfo -> ArgInfo -> ArgInfo Source #
Show ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ArgInfo -> ShowS Source # show :: ArgInfo -> String Source # showList :: [ArgInfo] -> ShowS Source #
NFData ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: ArgInfo -> () Source #
KillRange ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ArgInfo Source #
LensArgInfo ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getArgInfo :: ArgInfo -> ArgInfo Source # setArgInfo :: ArgInfo -> ArgInfo -> ArgInfo Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo Source #
LensFreeVariables ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getFreeVariables :: ArgInfo -> FreeVariables Source # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo Source #
LensOrigin ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getOrigin :: ArgInfo -> Origin Source # setOrigin :: Origin -> ArgInfo -> ArgInfo Source # mapOrigin :: (Origin -> Origin) -> ArgInfo -> ArgInfo Source #
LensRelevance ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getRelevance :: ArgInfo -> Relevance Source # setRelevance :: Relevance -> ArgInfo -> ArgInfo Source # mapRelevance :: (Relevance -> Relevance) -> ArgInfo -> ArgInfo Source #
LensQuantity ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getQuantity :: ArgInfo -> Quantity Source # setQuantity :: Quantity -> ArgInfo -> ArgInfo Source # mapQuantity :: (Quantity -> Quantity) -> ArgInfo -> ArgInfo Source #
LensModality ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getModality :: ArgInfo -> Modality Source # setModality :: Modality -> ArgInfo -> ArgInfo Source # mapModality :: (Modality -> Modality) -> ArgInfo -> ArgInfo Source #
LensHiding ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getHiding :: ArgInfo -> Hiding Source # setHiding :: Hiding -> ArgInfo -> ArgInfo Source # mapHiding :: (Hiding -> Hiding) -> ArgInfo -> ArgInfo Source #
EmbPrj ArgInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ArgInfo -> S Int32 Source # icod_ :: ArgInfo -> S Int32 Source # value :: Int32 -> R ArgInfo Source #
SynEq ArgInfo Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo) synEq' :: ArgInfo -> ArgInfo -> SynEqM (ArgInfo, ArgInfo)
ToTerm ArgInfo Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (ArgInfo -> Term) Source # toTermR :: TCM (ArgInfo -> ReduceM Term) Source #
Unquote ArgInfo Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM ArgInfo Source #

class LensArgInfo a where Source #

Minimal complete definition

getArgInfo

Methods

getArgInfo :: a -> ArgInfo Source #

setArgInfo :: ArgInfo -> a -> a Source #

mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a Source #

Instances

LensArgInfo ArgInfo Source # |
Instance details Defined in Agda.Syntax.Common Methods getArgInfo :: ArgInfo -> ArgInfo Source # setArgInfo :: ArgInfo -> ArgInfo -> ArgInfo Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo Source #
LensArgInfo (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getArgInfo :: Dom e -> ArgInfo Source # setArgInfo :: ArgInfo -> Dom e -> Dom e Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom e -> Dom e Source #
LensArgInfo (Arg a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getArgInfo :: Arg a -> ArgInfo Source # setArgInfo :: ArgInfo -> Arg a -> Arg a Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Arg a -> Arg a Source #

defaultArgInfo :: ArgInfo Source #

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 #

getFreeVariablesArgInfo :: LensArgInfo a => LensGet FreeVariables a Source #

setFreeVariablesArgInfo :: LensArgInfo a => LensSet FreeVariables a Source #

mapFreeVariablesArgInfo :: LensArgInfo a => LensMap FreeVariables a Source #

# Arguments

data Arg e Source #

Constructors

Arg |

Fields

- argInfo :: ArgInfo
- unArg :: e

Instances

Functor Arg Source # |
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> Arg a -> Arg b Source # (<$) :: a -> Arg b -> Arg a Source #
Foldable Arg Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => Arg m -> m Source #

foldMap :: Monoid m => (a -> m) -> Arg a -> m Source #

foldr :: (a -> b -> b) -> b -> Arg a -> b Source #

foldr' :: (a -> b -> b) -> b -> Arg a -> b Source #

foldl :: (b -> a -> b) -> b -> Arg a -> b Source #

foldl' :: (b -> a -> b) -> b -> Arg a -> b Source #

foldr1 :: (a -> a -> a) -> Arg a -> a Source #

foldl1 :: (a -> a -> a) -> Arg a -> a Source #

toList :: Arg a -> [a] Source #

null :: Arg a -> Bool Source #

length :: Arg a -> Int Source #

elem :: Eq a => a -> Arg a -> Bool Source #

maximum :: Ord a => Arg a -> a Source #

minimum :: Ord a => Arg a -> a Source #

sum :: Num a => Arg a -> a Source #

product :: Num a => Arg a -> a Source #

Traversable Arg Source # |
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> Arg a -> f (Arg b) Source # sequenceA :: Applicative f => Arg (f a) -> f (Arg a) Source # mapM :: Monad m => (a -> m b) -> Arg a -> m (Arg b) Source # sequence :: Monad m => Arg (m a) -> m (Arg a) Source #
Decoration Arg Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> Arg a -> m (Arg b) Source # distributeF :: Functor m => Arg (m a) -> m (Arg a) Source #
MapNamedArgPattern NAP Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
IsPrefixOf Args Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Args -> Args -> Maybe Elims Source #
UniverseBi Args Pattern Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Args -> [Pattern] Source #
UniverseBi Args Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Args -> [Term] Source #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
UniverseBi Declaration (NamedArg Pattern) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Pattern] Source #
UniverseBi Declaration (NamedArg LHSCore) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] Source #
UniverseBi Declaration (NamedArg Expr) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] Source #
UniverseBi Declaration (NamedArg BindName) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] Source #
LensNamed name a => LensNamed name (Arg a) Source # |
Instance details Defined in Agda.Syntax.Common Methods lensNamed :: Lens' (Maybe name) (Arg a) Source #
PatternVars a (NamedArg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)] Source #
PatternVars a (Arg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)] Source #
Subst t a => Subst t (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Arg a -> Arg a Source #
PatternLike a b => PatternLike a (Arg b) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Arg b -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b) Source #
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of `VarP`, and the closest surrounding `NamedArg`. Note: the `mapNamedArg` for `Pattern'` is not expressible simply by `fmap` or `traverse` etc., since `ConP` has `NamedArg` subpatterns, which are taken into account by `mapNamedArg`.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a) Source #
APatternLike a b => APatternLike a (Arg b) Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Arg b -> m Source # traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b) Source #
Conversion TOM (Arg Pattern) (Pat O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) Source #
Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg a -> TOM (Hiding, b) Source #
Eq a => Eq (Arg a) Source # | Ignores `Quantity`, `Relevance`, `Origin`, and `FreeVariables`. Ignores content of argument if `Irrelevant`.
Instance details Defined in Agda.Syntax.Common Methods (==) :: Arg a -> Arg a -> Bool Source # (/=) :: Arg a -> Arg a -> Bool Source #
Data e => Data (Arg e) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Arg e -> c (Arg e) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Arg e) Source #

toConstr :: Arg e -> Constr Source #

dataTypeOf :: Arg e -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Arg e)) Source #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Arg e)) Source #

gmapT :: (forall b. Data b => b -> b) -> Arg e -> Arg e Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Arg e -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Arg e -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Arg e -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Arg e -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Arg e -> m (Arg e) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Arg e -> m (Arg e) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Arg e -> m (Arg e) Source #

Ord e => Ord (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: Arg e -> Arg e -> Ordering Source # (<) :: Arg e -> Arg e -> Bool Source # (<=) :: Arg e -> Arg e -> Bool Source # (>) :: Arg e -> Arg e -> Bool Source # (>=) :: Arg e -> Arg e -> Bool Source # max :: Arg e -> Arg e -> Arg e Source # min :: Arg e -> Arg e -> Arg e Source #
Show e => Show (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Arg e -> ShowS Source # show :: Arg e -> String Source # showList :: [Arg e] -> ShowS Source #
NFData e => NFData (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Arg e -> () Source #
Pretty a => Pretty (Arg a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Arg a -> Doc Source # prettyPrec :: Int -> Arg a -> Doc Source # prettyList :: [Arg a] -> Doc Source #
KillRange a => KillRange (Arg a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Arg a) Source #
SetRange a => SetRange (Arg a) Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Arg a -> Arg a Source #
HasRange a => HasRange (Arg a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Arg a -> Range Source #
LensArgInfo (Arg a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getArgInfo :: Arg a -> ArgInfo Source # setArgInfo :: ArgInfo -> Arg a -> Arg a Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Arg a -> Arg a Source #
LensFreeVariables (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getFreeVariables :: Arg e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Arg e -> Arg e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e Source #
LensOrigin (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getOrigin :: Arg e -> Origin Source # setOrigin :: Origin -> Arg e -> Arg e Source # mapOrigin :: (Origin -> Origin) -> Arg e -> Arg e Source #
LensRelevance (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRelevance :: Arg e -> Relevance Source # setRelevance :: Relevance -> Arg e -> Arg e Source # mapRelevance :: (Relevance -> Relevance) -> Arg e -> Arg e Source #
LensQuantity (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getQuantity :: Arg e -> Quantity Source # setQuantity :: Quantity -> Arg e -> Arg e Source # mapQuantity :: (Quantity -> Quantity) -> Arg e -> Arg e Source #
LensModality (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getModality :: Arg e -> Modality Source # setModality :: Modality -> Arg e -> Arg e Source # mapModality :: (Modality -> Modality) -> Arg e -> Arg e Source #
LensHiding (Arg e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getHiding :: Arg e -> Hiding Source # setHiding :: Hiding -> Arg e -> Arg e Source # mapHiding :: (Hiding -> Hiding) -> Arg e -> Arg e Source #
IsProjP a => IsProjP (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source #
CPatternLike p => CPatternLike (Arg p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Arg p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Arg p -> m (Arg p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Arg p -> m (Arg p) Source #
IsWithP p => IsWithP (Arg p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Arg p -> Maybe (Arg p) Source #
ExprLike a => ExprLike (Arg a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Arg a -> Arg a Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Arg a -> m (Arg a) Source # foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m Source #
LensSort a => LensSort (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Arg a) Source # getSort :: Arg a -> Sort Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Arg a -> FV (Arg a) Source #
Free a => Free (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Arg a -> FreeM c Source #
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns.
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] Source # applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] Source #
TermLike a => TermLike (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Arg a -> m (Arg a) Source # foldTerm :: Monoid m => (Term -> m) -> Arg a -> m Source #
GetDefs a => GetDefs (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Arg a -> m () Source #
SubstExpr a => SubstExpr (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Arg a -> Arg a Source #
AllNames a => AllNames (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Arg a -> Seq QName Source #
CountPatternVars a => CountPatternVars (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Arg a -> Int Source #
ExprLike a => ExprLike (Arg a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Arg a -> m (Arg a) Source # foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Arg a -> m (Arg a) Source # mapExpr :: (Expr -> Expr) -> Arg a -> Arg a Source #
Free a => Free (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Arg a -> FreeT
EmbPrj a => EmbPrj (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Arg a -> S Int32 Source # icod_ :: Arg a -> S Int32 Source # value :: Int32 -> R (Arg a) Source #
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Arg a -> TCM Doc Source #
NamesIn a => NamesIn (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Arg a -> Set QName Source #
PiApplyM a => PiApplyM (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM :: MonadReduce m => Type -> Arg a -> m Type Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Arg a -> TCM Bool Source #
ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Arg a -> TCM (Arg a) Source #
MentionsMeta t => MentionsMeta (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Arg t -> Bool Source #
InstantiateFull t => InstantiateFull (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Arg t -> ReduceM (Arg t) Source #
Normalise t => Normalise (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Arg t -> ReduceM (Arg t) Source #
Simplify t => Simplify (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Arg t -> ReduceM (Arg t) Source #
Reduce t => Reduce (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Arg t -> ReduceM (Arg t) Source # reduceB' :: Arg t -> ReduceM (Blocked (Arg t)) Source #
Instantiate t => Instantiate (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Arg t -> ReduceM (Arg t) Source #
SynEq a => SynEq (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Arg a -> Arg a -> SynEqM (Arg a, Arg a) synEq' :: Arg a -> Arg a -> SynEqM (Arg a, Arg a)
(Reduce a, ForceNotFree a) => ForceNotFree (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Arg a -> m (Arg a)
SubstWithOrigin (Arg Term) Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term Source #
SubstWithOrigin (Arg DisplayTerm) Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg DisplayTerm -> Arg DisplayTerm Source #
Match a => Match (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Arg a -> Arg a -> MaybeT TCM [WithOrigin Term] Source #
UsableModality a => UsableModality (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Arg a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Arg a -> TCM Bool Source #
NormaliseProjP a => NormaliseProjP (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Arg a -> m (Arg a) Source #
ForcedVariables a => ForcedVariables (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Forcing Methods forcedVariables :: Arg a -> [(Modality, Nat)] Source #
ComputeOccurrences a => ComputeOccurrences (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Arg a -> OccM OccurrencesBuilder Source #
HasPolarity a => HasPolarity (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Arg a -> TCM [Polarity] Source #
FoldRigid a => FoldRigid (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Arg a -> TCM m Source #
Occurs a => Occurs (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Arg a -> TCM (Arg a) Source # metaOccurs :: MetaId -> Arg a -> TCM () Source #
ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: Arg a -> TCM (Arg a) Source #
NoProjectedVar a => NoProjectedVar (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Arg a -> Either ProjVarExc () Source #
Unquote a => Unquote (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM (Arg a) Source #
AbsTerm a => AbsTerm (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Arg a -> Arg a Source #
IsFlexiblePattern a => IsFlexiblePattern (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Arg a -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Arg a -> TCM Bool Source #
PatternVarModalities a x => PatternVarModalities (Arg a) x Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Arg a -> [(x, Modality)] Source #
TermToPattern a b => TermToPattern (Arg a) (Arg b) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Arg a -> TCM (Arg b) Source #
ToAbstract [Arg Term] [NamedArg Expr] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [Arg Term] -> WithNames [NamedArg Expr] Source #
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Arg r -> WithNames (NamedArg a) Source #
ToConcrete a c => ToConcrete (Arg a) (Arg c) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Arg a -> AbsToCon (Arg c) Source # bindToConcrete :: Arg a -> (Arg c -> AbsToCon b) -> AbsToCon b Source #
Reify i a => Reify (Dom i) (Arg a) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Dom i -> TCM (Arg a) Source # reifyWhen :: Bool -> Dom i -> TCM (Arg a) Source #
Reify i a => Reify (Arg i) (Arg a) Source # | Skip reification of implicit and irrelevant args if option is off.
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Arg i -> TCM (Arg a) Source # reifyWhen :: Bool -> Arg i -> TCM (Arg a) Source #
ToAbstract c a => ToAbstract (Arg c) (Arg a) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Arg c -> ScopeM (Arg a) Source #
LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: Arg a -> State [i] (Arg b) Source # unlabelPatVars :: Arg b -> Arg a Source #
Match t a b => Match (Dom t) (Arg a) (Arg b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM () Source #
PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b) Source #
AddContext ([NamedArg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
AddContext ([Arg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Arg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([Arg Name], Type) -> Nat Source #

defaultArg :: a -> Arg a Source #

withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #

`xs `withArgsFrom` args` translates `xs` into a list of `Arg`s, using the elements in `args` to fill in the non-`unArg` fields.

Precondition: The two lists should have equal length.

withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] Source #

# Names

class Eq a => Underscore a where Source #

Minimal complete definition

underscore

Methods

underscore :: a Source #

isUnderscore :: a -> Bool Source #

Instances

Underscore ByteString Source # |
Instance details Defined in Agda.Syntax.Common Methods underscore :: ByteString Source # isUnderscore :: ByteString -> Bool Source #
Underscore String Source # |
Instance details Defined in Agda.Syntax.Common Methods underscore :: String Source # isUnderscore :: String -> Bool Source #
Underscore Doc Source # |
Instance details Defined in Agda.Syntax.Common Methods underscore :: Doc Source # isUnderscore :: Doc -> Bool Source #
Underscore QName Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods underscore :: QName Source # isUnderscore :: QName -> Bool Source #
Underscore Name Source # |
Instance details Defined in Agda.Syntax.Concrete.Name Methods underscore :: Name Source # isUnderscore :: Name -> Bool Source #
Underscore Expr Source # |
Instance details Defined in Agda.Syntax.Abstract Methods underscore :: Expr Source # isUnderscore :: Expr -> Bool Source #

# Function type domain

data Dom e Source #

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 = True` for the domain of a `Pi` type, 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.

Constructors

Dom |

Fields

- domInfo :: ArgInfo
- domFinite :: !Bool
- domName :: Maybe RString
- unDom :: e

Instances

Functor Dom Source # |
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> Dom a -> Dom b Source # (<$) :: a -> Dom b -> Dom a Source #
Foldable Dom Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => Dom m -> m Source #

foldMap :: Monoid m => (a -> m) -> Dom a -> m Source #

foldr :: (a -> b -> b) -> b -> Dom a -> b Source #

foldr' :: (a -> b -> b) -> b -> Dom a -> b Source #

foldl :: (b -> a -> b) -> b -> Dom a -> b Source #

foldl' :: (b -> a -> b) -> b -> Dom a -> b Source #

foldr1 :: (a -> a -> a) -> Dom a -> a Source #

foldl1 :: (a -> a -> a) -> Dom a -> a Source #

toList :: Dom a -> [a] Source #

null :: Dom a -> Bool Source #

length :: Dom a -> Int Source #

elem :: Eq a => a -> Dom a -> Bool Source #

maximum :: Ord a => Dom a -> a Source #

minimum :: Ord a => Dom a -> a Source #

sum :: Num a => Dom a -> a Source #

product :: Num a => Dom a -> a Source #

Traversable Dom Source # |
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> Dom a -> f (Dom b) Source # sequenceA :: Applicative f => Dom (f a) -> f (Dom a) Source # mapM :: Monad m => (a -> m b) -> Dom a -> m (Dom b) Source # sequence :: Monad m => Dom (m a) -> m (Dom a) Source #
Decoration Dom Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> Dom a -> m (Dom b) Source # distributeF :: Functor m => Dom (m a) -> m (Dom a) Source #
TelToArgs ListTel Source # |
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: ListTel -> [Arg ArgName] Source #
TelToArgs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] Source #
Abstract Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope Source #
PrettyTCM Telescope Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Telescope -> TCM Doc Source #
TeleNoAbs ListTel Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: ListTel -> Term -> Term Source #
TeleNoAbs Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term Source #
DropArgs Telescope Source # | NOTE: This creates telescopes with unbound de Bruijn indices.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Telescope -> Telescope Source #
AddContext Telescope Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a Source # contextSize :: Telescope -> Nat Source #
Reduce Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
Instantiate Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Telescope -> ReduceM Telescope Source #
Reify Telescope Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Telescope0 -> TCM Telescope Source # reifyWhen :: Bool -> Telescope0 -> TCM Telescope Source #
Subst t a => Subst t (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Dom a -> Dom a Source #
Match t a b => Match t (Dom a) (Dom b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> t -> Dom a -> Dom b -> NLM () Source #
PatternFrom t a b => PatternFrom t (Dom a) (Dom b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> t -> Dom a -> TCM (Dom b) Source #
Eq a => Eq (Dom a) Source # | Ignores `Origin` and `FreeVariables`.
Instance details Defined in Agda.Syntax.Common Methods (==) :: Dom a -> Dom a -> Bool Source # (/=) :: Dom a -> Dom a -> Bool Source #
Data e => Data (Dom e) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Dom e -> c (Dom e) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Dom e) Source #

toConstr :: Dom e -> Constr Source #

dataTypeOf :: Dom e -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Dom e)) Source #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Dom e)) Source #

gmapT :: (forall b. Data b => b -> b) -> Dom e -> Dom e Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Dom e -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Dom e -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Dom e -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Dom e -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Dom e -> m (Dom e) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Dom e -> m (Dom e) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Dom e -> m (Dom e) Source #

Ord e => Ord (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: Dom e -> Dom e -> Ordering Source # (<) :: Dom e -> Dom e -> Bool Source # (<=) :: Dom e -> Dom e -> Bool Source # (>) :: Dom e -> Dom e -> Bool Source # (>=) :: Dom e -> Dom e -> Bool Source # max :: Dom e -> Dom e -> Dom e Source # min :: Dom e -> Dom e -> Dom e Source #
Show e => Show (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Dom e -> ShowS Source # show :: Dom e -> String Source # showList :: [Dom e] -> ShowS Source #
Pretty a => Pretty (Dom a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Dom a -> Doc Source # prettyPrec :: Int -> Dom a -> Doc Source # prettyList :: [Dom a] -> Doc Source #
Pretty a => Pretty (Tele (Dom a)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Tele (Dom a) -> Doc Source # prettyPrec :: Int -> Tele (Dom a) -> Doc Source # prettyList :: [Tele (Dom a)] -> Doc Source #
KillRange a => KillRange (Dom a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Dom a) Source #
HasRange a => HasRange (Dom a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Dom a -> Range Source #
LensArgInfo (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getArgInfo :: Dom e -> ArgInfo Source # setArgInfo :: ArgInfo -> Dom e -> Dom e Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom e -> Dom e Source #
LensFreeVariables (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getFreeVariables :: Dom e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Dom e -> Dom e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom e -> Dom e Source #
LensOrigin (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getOrigin :: Dom e -> Origin Source # setOrigin :: Origin -> Dom e -> Dom e Source # mapOrigin :: (Origin -> Origin) -> Dom e -> Dom e Source #
LensRelevance (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRelevance :: Dom e -> Relevance Source # setRelevance :: Relevance -> Dom e -> Dom e Source # mapRelevance :: (Relevance -> Relevance) -> Dom e -> Dom e Source #
LensQuantity (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getQuantity :: Dom e -> Quantity Source # setQuantity :: Quantity -> Dom e -> Dom e Source # mapQuantity :: (Quantity -> Quantity) -> Dom e -> Dom e Source #
LensModality (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getModality :: Dom e -> Modality Source # setModality :: Modality -> Dom e -> Dom e Source # mapModality :: (Modality -> Modality) -> Dom e -> Dom e Source #
LensHiding (Dom e) Source # |
Instance details Defined in Agda.Syntax.Common Methods getHiding :: Dom e -> Hiding Source # setHiding :: Hiding -> Dom e -> Dom e Source # mapHiding :: (Hiding -> Hiding) -> Dom e -> Dom e Source #
SgTel (Dom (ArgName, Type)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
SgTel (Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope Source #
LensSort a => LensSort (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Dom a) Source # getSort :: Dom a -> Sort Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Dom a -> FV (Dom a) Source #
Free a => Free (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Dom a -> FreeM c Source #
TermLike a => TermLike (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Dom a -> m (Dom a) Source # foldTerm :: Monoid m => (Term -> m) -> Dom a -> m Source #
GetDefs a => GetDefs (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Dom a -> m () Source #
Free a => Free (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Dom a -> FreeT
EmbPrj a => EmbPrj (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Dom a -> S Int32 Source # icod_ :: Dom a -> S Int32 Source # value :: Int32 -> R (Dom a) Source #
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Dom a -> TCM Doc Source #
NamesIn a => NamesIn (Dom a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Dom a -> Set QName Source #
IsSizeType a => IsSizeType (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: Dom a -> TCM (Maybe BoundedSize) Source #
AddContext (Dom (String, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (String, Type) -> tcm a -> tcm a Source # contextSize :: Dom (String, Type) -> Nat Source #
AddContext (Dom (Name, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a Source # contextSize :: Dom (Name, Type) -> Nat Source #
AddContext (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom Type -> tcm a -> tcm a Source # contextSize :: Dom Type -> Nat Source #
AddContext (KeepNames Telescope) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a Source # contextSize :: KeepNames Telescope -> Nat Source #
MentionsMeta t => MentionsMeta (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Dom t -> Bool Source #
InstantiateFull t => InstantiateFull (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Dom t -> ReduceM (Dom t) Source #
Normalise t => Normalise (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Dom t -> ReduceM (Dom t) Source #
Simplify t => Simplify (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Dom t -> ReduceM (Dom t) Source #
Reduce t => Reduce (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Dom t -> ReduceM (Dom t) Source # reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) Source #
Instantiate t => Instantiate (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Dom t -> ReduceM (Dom t) Source #
SynEq a => SynEq (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Dom a -> Dom a -> SynEqM (Dom a, Dom a) synEq' :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)
(Reduce a, ForceNotFree a) => ForceNotFree (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Dom a -> m (Dom a)
UsableModality a => UsableModality (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Dom a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Dom a -> TCM Bool Source #
ComputeOccurrences a => ComputeOccurrences (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Dom a -> OccM OccurrencesBuilder Source #
HasPolarity a => HasPolarity (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Dom a -> TCM [Polarity] Source #
FoldRigid a => FoldRigid (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Dom a -> TCM m Source #
Occurs a => Occurs (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Dom a -> TCM (Dom a) Source # metaOccurs :: MetaId -> Dom a -> TCM () Source #
Unquote a => Unquote (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM (Dom a) Source #
AbsTerm a => AbsTerm (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Dom a -> Dom a Source #
Reify i a => Reify (Dom i) (Arg a) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Dom i -> TCM (Arg a) Source # reifyWhen :: Bool -> Dom i -> TCM (Arg a) Source #
Match t a b => Match (Dom t) (Arg a) (Arg b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM () Source #
PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b) Source #
SgTel (ArgName, Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #
AddContext ([WithHiding Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext (String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (String, Dom Type) -> Nat Source #
AddContext (Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a Source # contextSize :: (Name, Dom Type) -> Nat Source #
AddContext (KeepNames String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (KeepNames String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (KeepNames String, Dom Type) -> Nat Source #
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Dom r, Name) -> WithNames TypedBinding Source #

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 #

defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a Source #

# Named arguments

data Named name a Source #

Something potentially carrying a name.

Constructors

Named |

Fields

- nameOf :: Maybe name
- namedThing :: a

Instances

MapNamedArgPattern NAP Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
UniverseBi Declaration (NamedArg Pattern) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Pattern] Source #
UniverseBi Declaration (NamedArg LHSCore) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] Source #
UniverseBi Declaration (NamedArg Expr) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] Source #
UniverseBi Declaration (NamedArg BindName) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] Source #
PatternVars a (NamedArg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)] Source #
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of `VarP`, and the closest surrounding `NamedArg`. Note: the `mapNamedArg` for `Pattern'` is not expressible simply by `fmap` or `traverse` etc., since `ConP` has `NamedArg` subpatterns, which are taken into account by `mapNamedArg`.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a) Source #
LensNamed name (Named name a) Source # |
Instance details Defined in Agda.Syntax.Common Methods lensNamed :: Lens' (Maybe name) (Named name a) Source #
Subst t a => Subst t (Named name a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Named name a -> Named name a Source #
PatternLike a b => PatternLike a (Named x b) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Named x b -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named x b -> m (Named x b) Source #
APatternLike a b => APatternLike a (Named n b) Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Named n b -> m Source # traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named n b -> m (Named n b) Source #
Functor (Named name) Source # |
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> Named name a -> Named name b Source # (<$) :: a -> Named name b -> Named name a Source #
Foldable (Named name) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => Named name m -> m Source #

foldMap :: Monoid m => (a -> m) -> Named name a -> m Source #

foldr :: (a -> b -> b) -> b -> Named name a -> b Source #

foldr' :: (a -> b -> b) -> b -> Named name a -> b Source #

foldl :: (b -> a -> b) -> b -> Named name a -> b Source #

foldl' :: (b -> a -> b) -> b -> Named name a -> b Source #

foldr1 :: (a -> a -> a) -> Named name a -> a Source #

foldl1 :: (a -> a -> a) -> Named name a -> a Source #

toList :: Named name a -> [a] Source #

null :: Named name a -> Bool Source #

length :: Named name a -> Int Source #

elem :: Eq a => a -> Named name a -> Bool Source #

maximum :: Ord a => Named name a -> a Source #

minimum :: Ord a => Named name a -> a Source #

sum :: Num a => Named name a -> a Source #

product :: Num a => Named name a -> a Source #

Traversable (Named name) Source # |
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> Named name a -> f (Named name b) Source # sequenceA :: Applicative f => Named name (f a) -> f (Named name a) Source # mapM :: Monad m => (a -> m b) -> Named name a -> m (Named name b) Source # sequence :: Monad m => Named name (m a) -> m (Named name a) Source #
Decoration (Named name) Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> Named name a -> m (Named name b) Source # distributeF :: Functor m => Named name (m a) -> m (Named name a) Source #
Pretty e => Pretty (Named_ e) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Named_ e -> Doc Source # prettyPrec :: Int -> Named_ e -> Doc Source # prettyList :: [Named_ e] -> Doc Source #
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns.
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] Source # applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] Source #
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Named_ a -> TCM Doc Source #
NormaliseProjP a => NormaliseProjP (Named_ a) Source # |
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source #
ToAbstract [Arg Term] [NamedArg Expr] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [Arg Term] -> WithNames [NamedArg Expr] Source #
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Arg r -> WithNames (NamedArg a) Source #
(Eq name, Eq a) => Eq (Named name a) Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Named name a -> Named name a -> Bool Source # (/=) :: Named name a -> Named name a -> Bool Source #
(Data name, Data a) => Data (Named name a) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Named name a -> c (Named name a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Named name a) Source #

toConstr :: Named name a -> Constr Source #

dataTypeOf :: Named name a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Named name a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Named name a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Named name a -> Named name a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Named name a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Named name a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) Source #

(Ord name, Ord a) => Ord (Named name a) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: Named name a -> Named name a -> Ordering Source #

(<) :: Named name a -> Named name a -> Bool Source #

(<=) :: Named name a -> Named name a -> Bool Source #

(>) :: Named name a -> Named name a -> Bool Source #

(>=) :: Named name a -> Named name a -> Bool Source #

max :: Named name a -> Named name a -> Named name a Source #

min :: Named name a -> Named name a -> Named name a Source #

(Show name, Show a) => Show (Named name a) Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Named name a -> ShowS Source # show :: Named name a -> String Source # showList :: [Named name a] -> ShowS Source #
(NFData name, NFData a) => NFData (Named name a) Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Named name a -> () Source #
(KillRange name, KillRange a) => KillRange (Named name a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Named name a) Source #
SetRange a => SetRange (Named name a) Source # |
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Named name a -> Named name a Source #
HasRange a => HasRange (Named name a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Named name a -> Range Source #
IsProjP a => IsProjP (Named n a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source #
CPatternLike p => CPatternLike (Named n p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Named n p -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Named n p -> m (Named n p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Named n p -> m (Named n p) Source #
IsWithP p => IsWithP (Named n p) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Named n p -> Maybe (Named n p) Source #
ExprLike a => ExprLike (Named name a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Named name a -> Named name a Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Named name a -> m (Named name a) Source # foldExpr :: Monoid m => (Expr -> m) -> Named name a -> m Source #
SubstExpr a => SubstExpr (Named name a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Named name a -> Named name a Source #
AllNames a => AllNames (Named name a) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: Named name a -> Seq QName Source #
CountPatternVars a => CountPatternVars (Named x a) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Named x a -> Int Source #
ExprLike a => ExprLike (Named x a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Named x a -> m (Named x a) Source # foldExpr :: Monoid m => (Expr -> m) -> Named x a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Named x a -> m (Named x a) Source # mapExpr :: (Expr -> Expr) -> Named x a -> Named x a Source #
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Named s t -> S Int32 Source # icod_ :: Named s t -> S Int32 Source # value :: Int32 -> R (Named s t) Source #
NamesIn a => NamesIn (Named n a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Named n a -> Set QName Source #
PiApplyM a => PiApplyM (Named n a) Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM :: MonadReduce m => Type -> Named n a -> m Type Source #
AddContext ([NamedArg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Named n a -> TCM (Named n a) Source #
InstantiateFull t => InstantiateFull (Named name t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Named name t -> ReduceM (Named name t) Source #
Normalise t => Normalise (Named name t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Named name t -> ReduceM (Named name t) Source #
Simplify t => Simplify (Named name t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Named name t -> ReduceM (Named name t) Source #
IsFlexiblePattern a => IsFlexiblePattern (Named name a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Named name a -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Named name a -> TCM Bool Source #
PatternVarModalities a x => PatternVarModalities (Named s a) x Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Named s a -> [(x, Modality)] Source #
TermToPattern a b => TermToPattern (Named c a) (Named c b) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Named c a -> TCM (Named c b) Source #
ToAbstract r a => ToAbstract (Named name r) (Named name a) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Named name r -> WithNames (Named name a) Source #
ToConcrete a c => ToConcrete (Named name a) (Named name c) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Named name a -> AbsToCon (Named name c) Source # bindToConcrete :: Named name a -> (Named name c -> AbsToCon b) -> AbsToCon b Source #
Reify i a => Reify (Named n i) (Named n a) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Named n i -> TCM (Named n a) Source # reifyWhen :: Bool -> Named n i -> TCM (Named n a) Source #
ToAbstract c a => ToAbstract (Named name c) (Named name a) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Named name c -> ScopeM (Named name a) Source #
LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: Named x a -> State [i] (Named x b) Source # unlabelPatVars :: Named x b -> Named x a Source #

type Named_ = Named RString Source #

Standard naming.

unnamed :: a -> Named name a Source #

named :: name -> a -> Named name a Source #

class LensNamed name a | a -> name where Source #

Accessor/editor for the `nameOf` component.

Methods

lensNamed :: Lens' (Maybe name) a Source #

Instances

LensNamed name a => LensNamed name (Arg a) Source # |
Instance details Defined in Agda.Syntax.Common Methods lensNamed :: Lens' (Maybe name) (Arg a) Source #
LensNamed name (Named name a) Source # |
Instance details Defined in Agda.Syntax.Common Methods lensNamed :: Lens' (Maybe name) (Named name a) Source #

getNameOf :: LensNamed name a => a -> Maybe name Source #

setNameOf :: LensNamed name a => Maybe name -> a -> a Source #

mapNameOf :: LensNamed name a => (Maybe name -> Maybe name) -> a -> a Source #

type NamedArg a = Arg (Named_ a) Source #

Only `Hidden` arguments can have names.

namedArg :: NamedArg a -> a Source #

Get the content of a `NamedArg`.

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.

data Ranged a Source #

Thing with range info.

Constructors

Ranged |

Fields

- rangeOf :: Range
- rangedThing :: a

Instances

Functor Ranged Source # |
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> Ranged a -> Ranged b Source # (<$) :: a -> Ranged b -> Ranged a Source #
Foldable Ranged Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => Ranged m -> m Source #

foldMap :: Monoid m => (a -> m) -> Ranged a -> m Source #

foldr :: (a -> b -> b) -> b -> Ranged a -> b Source #

foldr' :: (a -> b -> b) -> b -> Ranged a -> b Source #

foldl :: (b -> a -> b) -> b -> Ranged a -> b Source #

foldl' :: (b -> a -> b) -> b -> Ranged a -> b Source #

foldr1 :: (a -> a -> a) -> Ranged a -> a Source #

foldl1 :: (a -> a -> a) -> Ranged a -> a Source #

toList :: Ranged a -> [a] Source #

null :: Ranged a -> Bool Source #

length :: Ranged a -> Int Source #

elem :: Eq a => a -> Ranged a -> Bool Source #

maximum :: Ord a => Ranged a -> a Source #

minimum :: Ord a => Ranged a -> a Source #

sum :: Num a => Ranged a -> a Source #

product :: Num a => Ranged a -> a Source #

Traversable Ranged Source # |
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> Ranged a -> f (Ranged b) Source # sequenceA :: Applicative f => Ranged (f a) -> f (Ranged a) Source # mapM :: Monad m => (a -> m b) -> Ranged a -> m (Ranged b) Source # sequence :: Monad m => Ranged (m a) -> m (Ranged a) Source #
Decoration Ranged Source # |
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> Ranged a -> m (Ranged b) Source # distributeF :: Functor m => Ranged (m a) -> m (Ranged a) Source #
MapNamedArgPattern NAP Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
UniverseBi Declaration (NamedArg Pattern) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Pattern] Source #
UniverseBi Declaration (NamedArg LHSCore) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] Source #
UniverseBi Declaration (NamedArg Expr) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] Source #
UniverseBi Declaration (NamedArg BindName) Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] Source #
PatternVars a (NamedArg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)] Source #
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of `VarP`, and the closest surrounding `NamedArg`. Note: the `mapNamedArg` for `Pattern'` is not expressible simply by `fmap` or `traverse` etc., since `ConP` has `NamedArg` subpatterns, which are taken into account by `mapNamedArg`.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a) Source #
Eq a => Eq (Ranged a) Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Ranged a -> Ranged a -> Bool Source # (/=) :: Ranged a -> Ranged a -> Bool Source #
Data a => Data (Ranged a) Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ranged a) Source #

toConstr :: Ranged a -> Constr Source #

dataTypeOf :: Ranged a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Ranged a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ranged a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Ranged a -> Ranged a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Ranged a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ranged a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) Source #

Ord a => Ord (Ranged a) Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: Ranged a -> Ranged a -> Ordering Source # (<) :: Ranged a -> Ranged a -> Bool Source # (<=) :: Ranged a -> Ranged a -> Bool Source # (>) :: Ranged a -> Ranged a -> Bool Source # (>=) :: Ranged a -> Ranged a -> Bool Source # max :: Ranged a -> Ranged a -> Ranged a Source # min :: Ranged a -> Ranged a -> Ranged a Source #
Show a => Show (Ranged a) Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Ranged a -> ShowS Source # show :: Ranged a -> String Source # showList :: [Ranged a] -> ShowS Source #
NFData a => NFData (Ranged a) Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Common Methods rnf :: Ranged a -> () Source #
Pretty a => Pretty (Ranged a) Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Ranged a -> Doc Source # prettyPrec :: Int -> Ranged a -> Doc Source # prettyList :: [Ranged a] -> Doc Source #
Pretty e => Pretty (Named_ e) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Named_ e -> Doc Source # prettyPrec :: Int -> Named_ e -> Doc Source # prettyList :: [Named_ e] -> Doc Source #
KillRange (Ranged a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Ranged a) Source #
HasRange (Ranged a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Ranged a -> Range Source #
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns.
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] Source # applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] Source #
EmbPrj a => EmbPrj (Ranged a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Ranged a -> S Int32 Source # icod_ :: Ranged a -> S Int32 Source # value :: Int32 -> R (Ranged a) Source #
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Named_ a -> TCM Doc Source #
NormaliseProjP a => NormaliseProjP (Named_ a) Source # |
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source #
ToAbstract [Arg Term] [NamedArg Expr] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [Arg Term] -> WithNames [NamedArg Expr] Source #
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Arg r -> WithNames (NamedArg a) Source #
AddContext ([NamedArg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #

unranged :: a -> Ranged a Source #

Thing with no range info.

# Raw names (before parsing into name parts).

type RawName = String Source #

A `RawName` is some sort of string.

rawNameToString :: RawName -> String Source #

stringToRawName :: String -> RawName Source #

type RString = Ranged RawName Source #

String with range info.

# Further constructor and projection info

data ConOrigin Source #

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 # |
Instance details Defined in Agda.Syntax.Common Methods minBound :: ConOrigin Source # maxBound :: ConOrigin Source #
Enum ConOrigin Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: ConOrigin -> ConOrigin Source #

pred :: ConOrigin -> ConOrigin Source #

toEnum :: Int -> ConOrigin Source #

fromEnum :: ConOrigin -> Int Source #

enumFrom :: ConOrigin -> [ConOrigin] Source #

enumFromThen :: ConOrigin -> ConOrigin -> [ConOrigin] Source #

enumFromTo :: ConOrigin -> ConOrigin -> [ConOrigin] Source #

enumFromThenTo :: ConOrigin -> ConOrigin -> ConOrigin -> [ConOrigin] Source #

Eq ConOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: ConOrigin -> ConOrigin -> Bool Source # (/=) :: ConOrigin -> ConOrigin -> Bool Source #
Data ConOrigin Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConOrigin Source #

toConstr :: ConOrigin -> Constr Source #

dataTypeOf :: ConOrigin -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConOrigin) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConOrigin) Source #

gmapT :: (forall b. Data b => b -> b) -> ConOrigin -> ConOrigin Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ConOrigin -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConOrigin -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin Source #

Ord ConOrigin Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: ConOrigin -> ConOrigin -> Ordering Source #

(<) :: ConOrigin -> ConOrigin -> Bool Source #

(<=) :: ConOrigin -> ConOrigin -> Bool Source #

(>) :: ConOrigin -> ConOrigin -> Bool Source #

(>=) :: ConOrigin -> ConOrigin -> Bool Source #

max :: ConOrigin -> ConOrigin -> ConOrigin Source #

min :: ConOrigin -> ConOrigin -> ConOrigin Source #

Show ConOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ConOrigin -> ShowS Source # show :: ConOrigin -> String Source # showList :: [ConOrigin] -> ShowS Source #
KillRange ConOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ConOrigin Source #
EmbPrj ConOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ConOrigin -> S Int32 Source # icod_ :: ConOrigin -> S Int32 Source # value :: Int32 -> R 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 # |
Instance details Defined in Agda.Syntax.Common Methods minBound :: ProjOrigin Source # maxBound :: ProjOrigin Source #
Enum ProjOrigin Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: ProjOrigin -> ProjOrigin Source #

pred :: ProjOrigin -> ProjOrigin Source #

toEnum :: Int -> ProjOrigin Source #

fromEnum :: ProjOrigin -> Int Source #

enumFrom :: ProjOrigin -> [ProjOrigin] Source #

enumFromThen :: ProjOrigin -> ProjOrigin -> [ProjOrigin] Source #

enumFromTo :: ProjOrigin -> ProjOrigin -> [ProjOrigin] Source #

enumFromThenTo :: ProjOrigin -> ProjOrigin -> ProjOrigin -> [ProjOrigin] Source #

Eq ProjOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: ProjOrigin -> ProjOrigin -> Bool Source # (/=) :: ProjOrigin -> ProjOrigin -> Bool Source #
Data ProjOrigin Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProjOrigin Source #

toConstr :: ProjOrigin -> Constr Source #

dataTypeOf :: ProjOrigin -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProjOrigin) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProjOrigin) Source #

gmapT :: (forall b. Data b => b -> b) -> ProjOrigin -> ProjOrigin Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProjOrigin -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProjOrigin -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ProjOrigin -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProjOrigin -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin Source #

Ord ProjOrigin Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: ProjOrigin -> ProjOrigin -> Ordering Source #

(<) :: ProjOrigin -> ProjOrigin -> Bool Source #

(<=) :: ProjOrigin -> ProjOrigin -> Bool Source #

(>) :: ProjOrigin -> ProjOrigin -> Bool Source #

(>=) :: ProjOrigin -> ProjOrigin -> Bool Source #

max :: ProjOrigin -> ProjOrigin -> ProjOrigin Source #

min :: ProjOrigin -> ProjOrigin -> ProjOrigin Source #

Show ProjOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ProjOrigin -> ShowS Source # show :: ProjOrigin -> String Source # showList :: [ProjOrigin] -> ShowS Source #
KillRange ProjOrigin Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ProjOrigin Source #
EmbPrj ProjOrigin Source # |
Instance details 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 #

Constructors

IsData |
IsRecord |

Instances

Eq DataOrRecord Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: DataOrRecord -> DataOrRecord -> Bool Source # (/=) :: DataOrRecord -> DataOrRecord -> Bool Source #
Data DataOrRecord Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataOrRecord Source #

toConstr :: DataOrRecord -> Constr Source #

dataTypeOf :: DataOrRecord -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataOrRecord) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataOrRecord) Source #

gmapT :: (forall b. Data b => b -> b) -> DataOrRecord -> DataOrRecord Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DataOrRecord -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DataOrRecord -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord Source #

Ord DataOrRecord Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: DataOrRecord -> DataOrRecord -> Ordering Source #

(<) :: DataOrRecord -> DataOrRecord -> Bool Source #

(<=) :: DataOrRecord -> DataOrRecord -> Bool Source #

(>) :: DataOrRecord -> DataOrRecord -> Bool Source #

(>=) :: DataOrRecord -> DataOrRecord -> Bool Source #

max :: DataOrRecord -> DataOrRecord -> DataOrRecord Source #

min :: DataOrRecord -> DataOrRecord -> DataOrRecord Source #

Show DataOrRecord Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> DataOrRecord -> ShowS Source # show :: DataOrRecord -> String Source # showList :: [DataOrRecord] -> ShowS Source #
EmbPrj DataOrRecord Source # |
Instance details 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.

data IsInfix Source #

Functions can be defined in both infix and prefix style. See `LHS`.

Constructors

InfixDef |
PrefixDef |

Instances

Eq IsInfix Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsInfix -> IsInfix -> Bool Source # (/=) :: IsInfix -> IsInfix -> Bool Source #
Data IsInfix Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInfix Source #

toConstr :: IsInfix -> Constr Source #

dataTypeOf :: IsInfix -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInfix) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInfix) Source #

gmapT :: (forall b. Data b => b -> b) -> IsInfix -> IsInfix Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> IsInfix -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInfix -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix Source #

Ord IsInfix Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: IsInfix -> IsInfix -> Ordering Source # (<) :: IsInfix -> IsInfix -> Bool Source # (<=) :: IsInfix -> IsInfix -> Bool Source # (>) :: IsInfix -> IsInfix -> Bool Source # (>=) :: IsInfix -> IsInfix -> Bool Source # max :: IsInfix -> IsInfix -> IsInfix Source # min :: IsInfix -> IsInfix -> IsInfix Source #
Show IsInfix Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsInfix -> ShowS Source # show :: IsInfix -> String Source # showList :: [IsInfix] -> ShowS Source #

data Access Source #

Access modifier.

Constructors

PrivateAccess Origin | Store the `Origin` of the private block that lead to this qualifier. This is needed for more faithful printing of declarations.
PublicAccess |
OnlyQualified | Visible from outside, but not exported when opening the module Used for qualified constructors.

Instances

Eq Access Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Access -> Access -> Bool Source # (/=) :: Access -> Access -> Bool Source #
Data Access Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Access Source #

toConstr :: Access -> Constr Source #

dataTypeOf :: Access -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Access) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Access) Source #

gmapT :: (forall b. Data b => b -> b) -> Access -> Access Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Access -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Access -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Access -> m Access Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access Source #

Ord Access Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: Access -> Access -> Ordering Source # (<) :: Access -> Access -> Bool Source # (<=) :: Access -> Access -> Bool Source # (>) :: Access -> Access -> Bool Source # (>=) :: Access -> Access -> Bool Source # max :: Access -> Access -> Access Source # min :: Access -> Access -> Access Source #
Show Access Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Access -> ShowS Source # show :: Access -> String Source # showList :: [Access] -> ShowS Source #
NFData Access Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Access -> () Source #
Pretty Access Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: Access -> Doc Source # prettyPrec :: Int -> Access -> Doc Source # prettyList :: [Access] -> Doc Source #
KillRange Access Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Access Source #
HasRange Access Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Access -> Range Source #
EmbPrj Access Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Access -> S Int32 Source # icod_ :: Access -> S Int32 Source # value :: Int32 -> R Access Source #

data IsAbstract Source #

Abstract or concrete

Constructors

AbstractDef |
ConcreteDef |

Instances

Eq IsAbstract Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsAbstract -> IsAbstract -> Bool Source # (/=) :: IsAbstract -> IsAbstract -> Bool Source #
Data IsAbstract Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsAbstract Source #

toConstr :: IsAbstract -> Constr Source #

dataTypeOf :: IsAbstract -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsAbstract) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsAbstract) Source #

gmapT :: (forall b. Data b => b -> b) -> IsAbstract -> IsAbstract Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsAbstract -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsAbstract -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> IsAbstract -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsAbstract -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract Source #

Ord IsAbstract Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: IsAbstract -> IsAbstract -> Ordering Source #

(<) :: IsAbstract -> IsAbstract -> Bool Source #

(<=) :: IsAbstract -> IsAbstract -> Bool Source #

(>) :: IsAbstract -> IsAbstract -> Bool Source #

(>=) :: IsAbstract -> IsAbstract -> Bool Source #

max :: IsAbstract -> IsAbstract -> IsAbstract Source #

min :: IsAbstract -> IsAbstract -> IsAbstract Source #

Show IsAbstract Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsAbstract -> ShowS Source # show :: IsAbstract -> String Source # showList :: [IsAbstract] -> ShowS Source #
KillRange IsAbstract Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsAbstract Source #
EmbPrj IsAbstract Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsAbstract -> S Int32 Source # icod_ :: IsAbstract -> S Int32 Source # value :: Int32 -> R IsAbstract Source #

data IsInstance Source #

Is this definition eligible for instance search?

Constructors

InstanceDef |
NotInstanceDef |

Instances

Eq IsInstance Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsInstance -> IsInstance -> Bool Source # (/=) :: IsInstance -> IsInstance -> Bool Source #
Data IsInstance Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInstance Source #

toConstr :: IsInstance -> Constr Source #

dataTypeOf :: IsInstance -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInstance) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInstance) Source #

gmapT :: (forall b. Data b => b -> b) -> IsInstance -> IsInstance Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInstance -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInstance -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> IsInstance -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInstance -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance Source #

Ord IsInstance Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: IsInstance -> IsInstance -> Ordering Source #

(<) :: IsInstance -> IsInstance -> Bool Source #

(<=) :: IsInstance -> IsInstance -> Bool Source #

(>) :: IsInstance -> IsInstance -> Bool Source #

(>=) :: IsInstance -> IsInstance -> Bool Source #

max :: IsInstance -> IsInstance -> IsInstance Source #

min :: IsInstance -> IsInstance -> IsInstance Source #

Show IsInstance Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsInstance -> ShowS Source # show :: IsInstance -> String Source # showList :: [IsInstance] -> ShowS Source #
NFData IsInstance Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: IsInstance -> () Source #
KillRange IsInstance Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsInstance Source #
HasRange IsInstance Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: IsInstance -> Range Source #

data IsMacro Source #

Is this a macro definition?

Constructors

MacroDef |
NotMacroDef |

Instances

Eq IsMacro Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsMacro -> IsMacro -> Bool Source # (/=) :: IsMacro -> IsMacro -> Bool Source #
Data IsMacro Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsMacro Source #

toConstr :: IsMacro -> Constr Source #

dataTypeOf :: IsMacro -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsMacro) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsMacro) Source #

gmapT :: (forall b. Data b => b -> b) -> IsMacro -> IsMacro Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> IsMacro -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsMacro -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro Source #

Ord IsMacro Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: IsMacro -> IsMacro -> Ordering Source # (<) :: IsMacro -> IsMacro -> Bool Source # (<=) :: IsMacro -> IsMacro -> Bool Source # (>) :: IsMacro -> IsMacro -> Bool Source # (>=) :: IsMacro -> IsMacro -> Bool Source # max :: IsMacro -> IsMacro -> IsMacro Source # min :: IsMacro -> IsMacro -> IsMacro Source #
Show IsMacro Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsMacro -> ShowS Source # show :: IsMacro -> String Source # showList :: [IsMacro] -> ShowS Source #
KillRange IsMacro Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsMacro Source #
HasRange IsMacro Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: IsMacro -> Range Source #

type Nat = Int Source #

type Arity = Nat Source #

# NameId

data NameId Source #

The unique identifier of a name. Second argument is the top-level module identifier.

Constructors

NameId !Word64 !Word64 |

Instances

Enum NameId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: NameId -> NameId Source #

pred :: NameId -> NameId Source #

toEnum :: Int -> NameId Source #

fromEnum :: NameId -> Int Source #

enumFrom :: NameId -> [NameId] Source #

enumFromThen :: NameId -> NameId -> [NameId] Source #

enumFromTo :: NameId -> NameId -> [NameId] Source #

enumFromThenTo :: NameId -> NameId -> NameId -> [NameId] Source #

Eq NameId Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: NameId -> NameId -> Bool Source # (/=) :: NameId -> NameId -> Bool Source #
Data NameId Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameId Source #

toConstr :: NameId -> Constr Source #

dataTypeOf :: NameId -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameId) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameId) Source #

gmapT :: (forall b. Data b => b -> b) -> NameId -> NameId Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NameId -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameId -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameId -> m NameId Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId Source #

Ord NameId Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: NameId -> NameId -> Ordering Source # (<) :: NameId -> NameId -> Bool Source # (<=) :: NameId -> NameId -> Bool Source # (>) :: NameId -> NameId -> Bool Source # (>=) :: NameId -> NameId -> Bool Source # max :: NameId -> NameId -> NameId Source # min :: NameId -> NameId -> NameId Source #
Show NameId Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> NameId -> ShowS Source # show :: NameId -> String Source # showList :: [NameId] -> ShowS Source #
Generic NameId Source # |
Instance details Defined in Agda.Syntax.Common Associated Types type Rep NameId :: Type -> Type Source # Methods from :: NameId -> Rep NameId x Source # to :: Rep NameId x -> NameId Source #
Hashable NameId Source # |
Instance details Defined in Agda.Syntax.Common Methods hashWithSalt :: Int -> NameId -> Int Source # hash :: NameId -> Int Source #
NFData NameId Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: NameId -> () Source #
Pretty NameId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: NameId -> Doc Source # prettyPrec :: Int -> NameId -> Doc Source # prettyList :: [NameId] -> Doc Source #
KillRange NameId Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT NameId Source #
HasFresh NameId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' NameId TCState Source # nextFresh' :: NameId -> NameId Source #
EmbPrj NameId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: NameId -> S Int32 Source # icod_ :: NameId -> S Int32 Source # value :: Int32 -> R NameId Source #
type Rep NameId Source # |
Instance details Defined in Agda.Syntax.Common type Rep NameId = D1 (MetaData "NameId" "Agda.Syntax.Common" "Agda-2.6.0.1-1X7fHcR3xPHzuc9vp1IMb" 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

newtype MetaId Source #

A meta variable identifier is just a natural number.

Constructors

MetaId |

Fields

- metaId :: Nat

Instances

Enum MetaId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: MetaId -> MetaId Source #

pred :: MetaId -> MetaId Source #

toEnum :: Int -> MetaId Source #

fromEnum :: MetaId -> Int Source #

enumFrom :: MetaId -> [MetaId] Source #

enumFromThen :: MetaId -> MetaId -> [MetaId] Source #

enumFromTo :: MetaId -> MetaId -> [MetaId] Source #

enumFromThenTo :: MetaId -> MetaId -> MetaId -> [MetaId] Source #

Eq MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: MetaId -> MetaId -> Bool Source # (/=) :: MetaId -> MetaId -> Bool Source #
Integral MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods quot :: MetaId -> MetaId -> MetaId Source # rem :: MetaId -> MetaId -> MetaId Source # div :: MetaId -> MetaId -> MetaId Source # mod :: MetaId -> MetaId -> MetaId Source # quotRem :: MetaId -> MetaId -> (MetaId, MetaId) Source # divMod :: MetaId -> MetaId -> (MetaId, MetaId) Source # toInteger :: MetaId -> Integer Source #
Data MetaId Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaId Source #

toConstr :: MetaId -> Constr Source #

dataTypeOf :: MetaId -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaId) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaId) Source #

gmapT :: (forall b. Data b => b -> b) -> MetaId -> MetaId Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> MetaId -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaId -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId Source #

Num MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods (+) :: MetaId -> MetaId -> MetaId Source # (-) :: MetaId -> MetaId -> MetaId Source # (*) :: MetaId -> MetaId -> MetaId Source # negate :: MetaId -> MetaId Source # abs :: MetaId -> MetaId Source # signum :: MetaId -> MetaId Source # fromInteger :: Integer -> MetaId Source #
Ord MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: MetaId -> MetaId -> Ordering Source # (<) :: MetaId -> MetaId -> Bool Source # (<=) :: MetaId -> MetaId -> Bool Source # (>) :: MetaId -> MetaId -> Bool Source # (>=) :: MetaId -> MetaId -> Bool Source # max :: MetaId -> MetaId -> MetaId Source # min :: MetaId -> MetaId -> MetaId Source #
Real MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods toRational :: MetaId -> Rational Source #
Show MetaId Source # | Show non-record version of this newtype.
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> MetaId -> ShowS Source # show :: MetaId -> String Source # showList :: [MetaId] -> ShowS Source #
NFData MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: MetaId -> () Source #
Pretty MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: MetaId -> Doc Source # prettyPrec :: Int -> MetaId -> Doc Source # prettyList :: [MetaId] -> Doc Source #
GetDefs MetaId Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => MetaId -> m () Source #
HasFresh MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' MetaId TCState Source # nextFresh' :: MetaId -> MetaId Source #
EmbPrj MetaId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: MetaId -> S Int32 Source # icod_ :: MetaId -> S Int32 Source # value :: Int32 -> R MetaId Source #
PrettyTCM MetaId Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MetaId -> TCM Doc Source #
UnFreezeMeta MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MetaId -> TCM () Source #
IsInstantiatedMeta MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: MetaId -> TCM Bool Source #
FromTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction MetaId) Source #
ToTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (MetaId -> Term) Source # toTermR :: TCM (MetaId -> ReduceM Term) Source #
PrimTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: MetaId -> TCM Term Source #
Unquote MetaId Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM MetaId Source #
Reify MetaId Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MetaId -> TCM Expr Source # reifyWhen :: Bool -> MetaId -> TCM Expr Source #

newtype Constr a Source #

Constructors

Constr a |

Instances

ToConcrete (Constr Constructor) Declaration Source # |
Instance details 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: `_foo`.
Middle | The following underscore is in the middle of the name: `foo_bar`.
End | The following underscore is at the end of the name: `foo_`.

Instances

Eq PositionInName Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: PositionInName -> PositionInName -> Bool Source # (/=) :: PositionInName -> PositionInName -> Bool Source #
Data PositionInName Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PositionInName Source #

toConstr :: PositionInName -> Constr Source #

dataTypeOf :: PositionInName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PositionInName) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PositionInName) Source #

gmapT :: (forall b. Data b => b -> b) -> PositionInName -> PositionInName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> PositionInName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PositionInName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName Source #

Ord PositionInName Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: PositionInName -> PositionInName -> Ordering Source #

(<) :: PositionInName -> PositionInName -> Bool Source #

(<=) :: PositionInName -> PositionInName -> Bool Source #

(>) :: PositionInName -> PositionInName -> Bool Source #

(>=) :: PositionInName -> PositionInName -> Bool Source #

max :: PositionInName -> PositionInName -> PositionInName Source #

min :: PositionInName -> PositionInName -> PositionInName Source #

Show PositionInName Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> PositionInName -> ShowS Source # show :: PositionInName -> String Source # showList :: [PositionInName] -> ShowS Source #

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

Functor MaybePlaceholder Source # |
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b Source # (<$) :: a -> MaybePlaceholder b -> MaybePlaceholder a Source #
Foldable MaybePlaceholder Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

fold :: Monoid m => MaybePlaceholder m -> m Source #

foldMap :: Monoid m => (a -> m) -> MaybePlaceholder a -> m Source #

foldr :: (a -> b -> b) -> b -> MaybePlaceholder a -> b Source #

foldr' :: (a -> b -> b) -> b -> MaybePlaceholder a -> b Source #

foldl :: (b -> a -> b) -> b -> MaybePlaceholder a -> b Source #

foldl' :: (b -> a -> b) -> b -> MaybePlaceholder a -> b Source #

foldr1 :: (a -> a -> a) -> MaybePlaceholder a -> a Source #

foldl1 :: (a -> a -> a) -> MaybePlaceholder a -> a Source #

toList :: MaybePlaceholder a -> [a] Source #

null :: MaybePlaceholder a -> Bool Source #

length :: MaybePlaceholder a -> Int Source #

elem :: Eq a => a -> MaybePlaceholder a -> Bool Source #

maximum :: Ord a => MaybePlaceholder a -> a Source #

minimum :: Ord a => MaybePlaceholder a -> a Source #

sum :: Num a => MaybePlaceholder a -> a Source #

product :: Num a => MaybePlaceholder a -> a Source #

Traversable MaybePlaceholder Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

traverse :: Applicative f => (a -> f b) -> MaybePlaceholder a -> f (MaybePlaceholder b) Source #

sequenceA :: Applicative f => MaybePlaceholder (f a) -> f (MaybePlaceholder a) Source #

mapM :: Monad m => (a -> m b) -> MaybePlaceholder a -> m (MaybePlaceholder b) Source #

sequence :: Monad m => MaybePlaceholder (m a) -> m (MaybePlaceholder a) Source #

Eq e => Eq (MaybePlaceholder e) Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source # (/=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source #
Data e => Data (MaybePlaceholder e) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MaybePlaceholder e -> c (MaybePlaceholder e) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MaybePlaceholder e) Source #

toConstr :: MaybePlaceholder e -> Constr Source #

dataTypeOf :: MaybePlaceholder e -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (MaybePlaceholder e)) Source #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (MaybePlaceholder e)) Source #

gmapT :: (forall b. Data b => b -> b) -> MaybePlaceholder e -> MaybePlaceholder e Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MaybePlaceholder e -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MaybePlaceholder e -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> MaybePlaceholder e -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MaybePlaceholder e -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e) Source #

Ord e => Ord (MaybePlaceholder e) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: MaybePlaceholder e -> MaybePlaceholder e -> Ordering Source #

(<) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source #

(<=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source #

(>) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source #

(>=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool Source #

max :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e Source #

min :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e Source #

Show e => Show (MaybePlaceholder e) Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> MaybePlaceholder e -> ShowS Source # show :: MaybePlaceholder e -> String Source # showList :: [MaybePlaceholder e] -> ShowS Source #
NFData a => NFData (MaybePlaceholder a) Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: MaybePlaceholder a -> () Source #
Pretty a => Pretty (MaybePlaceholder a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: MaybePlaceholder a -> Doc Source # prettyPrec :: Int -> MaybePlaceholder a -> Doc Source # prettyList :: [MaybePlaceholder a] -> Doc Source #
KillRange a => KillRange (MaybePlaceholder a) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (MaybePlaceholder a) Source #
HasRange a => HasRange (MaybePlaceholder a) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: MaybePlaceholder a -> Range Source #
ExprLike a => ExprLike (MaybePlaceholder a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> MaybePlaceholder a -> MaybePlaceholder a Source # traverseExpr :: Monad m => (Expr -> m Expr) -> MaybePlaceholder a -> m (MaybePlaceholder a) Source # foldExpr :: Monoid m => (Expr -> m) -> MaybePlaceholder a -> m Source #

noPlaceholder :: e -> MaybePlaceholder e Source #

An abbreviation: `noPlaceholder = `NoPlaceholder` `Nothing``.

# Interaction meta variables

newtype InteractionId Source #

Constructors

InteractionId |

Fields

- interactionId :: Nat

Instances

Enum InteractionId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: InteractionId -> InteractionId Source #

pred :: InteractionId -> InteractionId Source #

toEnum :: Int -> InteractionId Source #

fromEnum :: InteractionId -> Int Source #

enumFrom :: InteractionId -> [InteractionId] Source #

enumFromThen :: InteractionId -> InteractionId -> [InteractionId] Source #

enumFromTo :: InteractionId -> InteractionId -> [InteractionId] Source #

enumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId] Source #

Eq InteractionId Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: InteractionId -> InteractionId -> Bool Source # (/=) :: InteractionId -> InteractionId -> Bool Source #
Integral InteractionId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

quot :: InteractionId -> InteractionId -> InteractionId Source #

rem :: InteractionId -> InteractionId -> InteractionId Source #

div :: InteractionId -> InteractionId -> InteractionId Source #

mod :: InteractionId -> InteractionId -> InteractionId Source #

quotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId) Source #

divMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId) Source #

toInteger :: InteractionId -> Integer Source #

Data InteractionId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InteractionId -> c InteractionId Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InteractionId Source #

toConstr :: InteractionId -> Constr Source #

dataTypeOf :: InteractionId -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InteractionId) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InteractionId) Source #

gmapT :: (forall b. Data b => b -> b) -> InteractionId -> InteractionId Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InteractionId -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InteractionId -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> InteractionId -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> InteractionId -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId Source #

Num InteractionId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

(+) :: InteractionId -> InteractionId -> InteractionId Source #

(-) :: InteractionId -> InteractionId -> InteractionId Source #

(*) :: InteractionId -> InteractionId -> InteractionId Source #

negate :: InteractionId -> InteractionId Source #

abs :: InteractionId -> InteractionId Source #

signum :: InteractionId -> InteractionId Source #

fromInteger :: Integer -> InteractionId Source #

Ord InteractionId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: InteractionId -> InteractionId -> Ordering Source #

(<) :: InteractionId -> InteractionId -> Bool Source #

(<=) :: InteractionId -> InteractionId -> Bool Source #

(>) :: InteractionId -> InteractionId -> Bool Source #

(>=) :: InteractionId -> InteractionId -> Bool Source #

max :: InteractionId -> InteractionId -> InteractionId Source #

min :: InteractionId -> InteractionId -> InteractionId Source #

Read InteractionId Source # |
Instance details Defined in Agda.Interaction.InteractionTop Methods readsPrec :: Int -> ReadS InteractionId Source # readList :: ReadS [InteractionId] Source # readPrec :: ReadPrec InteractionId Source # readListPrec :: ReadPrec [InteractionId] Source #
Real InteractionId Source # |
Instance details Defined in Agda.Syntax.Common Methods toRational :: InteractionId -> Rational Source #
Show InteractionId Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> InteractionId -> ShowS Source # show :: InteractionId -> String Source # showList :: [InteractionId] -> ShowS Source #
ToJSON InteractionId Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: InteractionId -> Value Source # toEncoding :: InteractionId -> Encoding Source # toJSONList :: [InteractionId] -> Value Source # toEncodingList :: [InteractionId] -> Encoding Source #
Pretty InteractionId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: InteractionId -> Doc Source # prettyPrec :: Int -> InteractionId -> Doc Source # prettyList :: [InteractionId] -> Doc Source #
KillRange InteractionId Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT InteractionId Source #
HasFresh InteractionId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' InteractionId TCState Source # nextFresh' :: InteractionId -> InteractionId Source #
ToConcrete InteractionId Expr Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: InteractionId -> AbsToCon Expr Source # bindToConcrete :: InteractionId -> (Expr -> AbsToCon b) -> AbsToCon b 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

- importDirRange :: Range
- using :: Using' n m
- hiding :: [ImportedName' n m]
- impRenaming :: [Renaming' n m]
- publicOpen :: Bool

  Only for `open`. Exports the opened names from the current module.

Instances

(Eq m, Eq n) => Eq (ImportDirective' n m) Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: ImportDirective' n m -> ImportDirective' n m -> Bool Source # (/=) :: ImportDirective' n m -> ImportDirective' n m -> Bool Source #
(Data n, Data m) => Data (ImportDirective' n m) Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportDirective' n m) Source #

toConstr :: ImportDirective' n m -> Constr Source #

dataTypeOf :: ImportDirective' n m -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportDirective' n m)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportDirective' n m)) Source #

gmapT :: (forall b. Data b => b -> b) -> ImportDirective' n m -> ImportDirective' n m Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ImportDirective' n m -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportDirective' n m -> u Source #

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) Source #

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) Source #

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) Source #

(Show a, Show b) => Show (ImportDirective' a b) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ImportDirective' a b -> ShowS Source # show :: ImportDirective' a b -> String Source # showList :: [ImportDirective' a b] -> ShowS Source #
(NFData a, NFData b) => NFData (ImportDirective' a b) Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Common Methods rnf :: ImportDirective' a b -> () Source #
(Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # |
Instance details 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 # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportDirective' a b) Source #
(HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: ImportDirective' a b -> Range Source #

data Using' n m Source #

Constructors

UseEverything |
Using [ImportedName' n m] |

Instances

(Eq m, Eq n) => Eq (Using' n m) Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Using' n m -> Using' n m -> Bool Source # (/=) :: Using' n m -> Using' n m -> Bool Source #
(Data n, Data m) => Data (Using' n m) Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Using' n m) Source #

toConstr :: Using' n m -> Constr Source #

dataTypeOf :: Using' n m -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Using' n m)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Using' n m)) Source #

gmapT :: (forall b. Data b => b -> b) -> Using' n m -> Using' n m Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Using' n m -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Using' n m -> u Source #

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) Source #

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) Source #

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) Source #

(Show a, Show b) => Show (Using' a b) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Using' a b -> ShowS Source # show :: Using' a b -> String Source # showList :: [Using' a b] -> ShowS Source #
Semigroup (Using' n m) Source # |
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Using' n m -> Using' n m -> Using' n m Source # sconcat :: NonEmpty (Using' n m) -> Using' n m Source # stimes :: Integral b => b -> Using' n m -> Using' n m Source #
Monoid (Using' n m) Source # |
Instance details Defined in Agda.Syntax.Common Methods mempty :: Using' n m Source # mappend :: Using' n m -> Using' n m -> Using' n m Source # mconcat :: [Using' n m] -> Using' n m Source #
(NFData a, NFData b) => NFData (Using' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: Using' a b -> () Source #
(Pretty a, Pretty b) => Pretty (Using' a b) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Using' a b -> Doc Source # prettyPrec :: Int -> Using' a b -> Doc Source # prettyList :: [Using' a b] -> Doc Source #
(KillRange a, KillRange b) => KillRange (Using' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Using' a b) Source #
(HasRange a, HasRange b) => HasRange (Using' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Using' 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 #

data ImportedName' n m Source #

An imported name can be a module or a defined name.

Constructors

ImportedModule m | Imported module name of type `m`.
ImportedName n | Imported name of type `n`.

Instances

(Eq m, Eq n) => Eq (ImportedName' n m) Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: ImportedName' n m -> ImportedName' n m -> Bool Source # (/=) :: ImportedName' n m -> ImportedName' n m -> Bool Source #
(Data n, Data m) => Data (ImportedName' n m) Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportedName' n m) Source #

toConstr :: ImportedName' n m -> Constr Source #

dataTypeOf :: ImportedName' n m -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportedName' n m)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportedName' n m)) Source #

gmapT :: (forall b. Data b => b -> b) -> ImportedName' n m -> ImportedName' n m Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ImportedName' n m -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportedName' n m -> u Source #

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) Source #

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) Source #

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) Source #

(Ord m, Ord n) => Ord (ImportedName' n m) Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: ImportedName' n m -> ImportedName' n m -> Ordering Source #

(<) :: ImportedName' n m -> ImportedName' n m -> Bool Source #

(<=) :: ImportedName' n m -> ImportedName' n m -> Bool Source #

(>) :: ImportedName' n m -> ImportedName' n m -> Bool Source #

(>=) :: ImportedName' n m -> ImportedName' n m -> Bool Source #

max :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m Source #

min :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m Source #

(Show m, Show n) => Show (ImportedName' n m) Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ImportedName' n m -> ShowS Source # show :: ImportedName' n m -> String Source # showList :: [ImportedName' n m] -> ShowS Source #
(NFData a, NFData b) => NFData (ImportedName' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: ImportedName' a b -> () Source #
(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # |
Instance details 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 # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportedName' a b) Source #
(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: ImportedName' a b -> Range Source #
(EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # |
Instance details 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 #

data Renaming' n m Source #

Constructors

Renaming |

Fields

- renFrom :: ImportedName' n m

  Rename from this name.

- renTo :: ImportedName' n m

  To this one. Must be same kind as `renFrom`.

- renToRange :: Range

  The range of the "to" keyword. Retained for highlighting purposes.

Instances

(Eq m, Eq n) => Eq (Renaming' n m) Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: Renaming' n m -> Renaming' n m -> Bool Source # (/=) :: Renaming' n m -> Renaming' n m -> Bool Source #
(Data n, Data m) => Data (Renaming' n m) Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Renaming' n m) Source #

toConstr :: Renaming' n m -> Constr Source #

dataTypeOf :: Renaming' n m -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Renaming' n m)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Renaming' n m)) Source #

gmapT :: (forall b. Data b => b -> b) -> Renaming' n m -> Renaming' n m Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Renaming' n m -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Renaming' n m -> u Source #

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) Source #

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) Source #

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) Source #

(Show a, Show b) => Show (Renaming' a b) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Renaming' a b -> ShowS Source # show :: Renaming' a b -> String Source # showList :: [Renaming' a b] -> ShowS Source #
(NFData a, NFData b) => NFData (Renaming' a b) Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Common Methods rnf :: Renaming' a b -> () Source #
(KillRange a, KillRange b) => KillRange (Renaming' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Renaming' a b) Source #
(HasRange a, HasRange b) => HasRange (Renaming' a b) Source # |
Instance details Defined in Agda.Syntax.Common Methods getRange :: Renaming' a b -> Range 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 `NoTerminationCheck`.
TerminationMeasure Range m | Skip termination checking but use measure instead.

Instances

Functor TerminationCheck Source # |
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> TerminationCheck a -> TerminationCheck b Source # (<$) :: a -> TerminationCheck b -> TerminationCheck a Source #
Eq m => Eq (TerminationCheck m) Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: TerminationCheck m -> TerminationCheck m -> Bool Source # (/=) :: TerminationCheck m -> TerminationCheck m -> Bool Source #
Data m => Data (TerminationCheck m) Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TerminationCheck m) Source #

toConstr :: TerminationCheck m -> Constr Source #

dataTypeOf :: TerminationCheck m -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TerminationCheck m)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TerminationCheck m)) Source #

gmapT :: (forall b. Data b => b -> b) -> TerminationCheck m -> TerminationCheck m Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TerminationCheck m -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TerminationCheck m -> u Source #

gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) Source #

gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) Source #

gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) Source #

Show m => Show (TerminationCheck m) Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> TerminationCheck m -> ShowS Source # show :: TerminationCheck m -> String Source # showList :: [TerminationCheck m] -> ShowS Source #
NFData a => NFData (TerminationCheck a) Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: TerminationCheck a -> () Source #
KillRange m => KillRange (TerminationCheck m) Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (TerminationCheck m) Source #

# Positivity

type PositivityCheck = Bool Source #

Positivity check? (Default = True).

# Universe checking

data UniverseCheck Source #

Universe check? (Default is yes).

Constructors

YesUniverseCheck |
NoUniverseCheck |

Instances

Bounded UniverseCheck Source # |
Instance details Defined in Agda.Syntax.Common Methods minBound :: UniverseCheck Source # maxBound :: UniverseCheck Source #
Enum UniverseCheck Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: UniverseCheck -> UniverseCheck Source #

pred :: UniverseCheck -> UniverseCheck Source #

toEnum :: Int -> UniverseCheck Source #

fromEnum :: UniverseCheck -> Int Source #

enumFrom :: UniverseCheck -> [UniverseCheck] Source #

enumFromThen :: UniverseCheck -> UniverseCheck -> [UniverseCheck] Source #

enumFromTo :: UniverseCheck -> UniverseCheck -> [UniverseCheck] Source #

enumFromThenTo :: UniverseCheck -> UniverseCheck -> UniverseCheck -> [UniverseCheck] Source #

Eq UniverseCheck Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: UniverseCheck -> UniverseCheck -> Bool Source # (/=) :: UniverseCheck -> UniverseCheck -> Bool Source #
Data UniverseCheck Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UniverseCheck -> c UniverseCheck Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UniverseCheck Source #

toConstr :: UniverseCheck -> Constr Source #

dataTypeOf :: UniverseCheck -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UniverseCheck) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UniverseCheck) Source #

gmapT :: (forall b. Data b => b -> b) -> UniverseCheck -> UniverseCheck Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> UniverseCheck -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UniverseCheck -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck Source #

Ord UniverseCheck Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

compare :: UniverseCheck -> UniverseCheck -> Ordering Source #

(<) :: UniverseCheck -> UniverseCheck -> Bool Source #

(<=) :: UniverseCheck -> UniverseCheck -> Bool Source #

(>) :: UniverseCheck -> UniverseCheck -> Bool Source #

(>=) :: UniverseCheck -> UniverseCheck -> Bool Source #

max :: UniverseCheck -> UniverseCheck -> UniverseCheck Source #

min :: UniverseCheck -> UniverseCheck -> UniverseCheck Source #

Show UniverseCheck Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> UniverseCheck -> ShowS Source # show :: UniverseCheck -> String Source # showList :: [UniverseCheck] -> ShowS Source #
KillRange UniverseCheck Source # |
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT UniverseCheck Source #