Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Common

Contents

Delayed
File
Eta-equality
Induction
Hiding
Modalities
Quantities
- Quantity origin.
- Quantity.
Relevance
Cohesion
Origin of arguments (user-written, inserted or reflected)
Free variable annotations
Argument decoration
Arguments
Names
Named arguments
- ArgName
Range decoration.
Raw names (before parsing into name parts).
Further constructor and projection info
Infixity, access, abstract, etc.
- private blocks, public imports
- abstract blocks
- instance blocks
- macro blocks
NameId
Meta variables
Placeholders (used to parse sections)
Interaction meta variables
Fixity
Notation coupled with Fixity
Import directive
- HasRange instances
- KillRange instances
- NFData instances
Termination
Positivity
Universe checking
Universe checking
Rewrite Directives on the LHS
Information on expanded ellipsis (...)

Description

Some common syntactic entities are defined in this module.

Synopsis

type Nat = Int
type Arity = Nat
data Delayed
- = 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
- modCohesion :: Cohesion
}
defaultModality :: Modality
moreUsableModality :: Modality -> Modality -> Bool
usableModality :: LensModality a => a -> Bool
composeModality :: Modality -> Modality -> Modality
applyModality :: LensModality a => Modality -> a -> a
inverseComposeModality :: Modality -> Modality -> Modality
inverseApplyModality :: LensModality a => Modality -> a -> a
addModality :: Modality -> Modality -> Modality
zeroModality :: Modality
topModality :: Modality
sameModality :: (LensModality a, LensModality b) => a -> b -> Bool
lModRelevance :: Lens' Relevance Modality
lModQuantity :: Lens' Quantity Modality
lModCohesion :: Lens' Cohesion Modality
class LensModality a where
- getModality :: a -> Modality
- setModality :: Modality -> a -> a
- mapModality :: (Modality -> Modality) -> a -> a
getRelevanceMod :: LensModality a => LensGet Relevance a
setRelevanceMod :: LensModality a => LensSet Relevance a
mapRelevanceMod :: LensModality a => LensMap Relevance a
getQuantityMod :: LensModality a => LensGet Quantity a
setQuantityMod :: LensModality a => LensSet Quantity a
mapQuantityMod :: LensModality a => LensMap Quantity a
getCohesionMod :: LensModality a => LensGet Cohesion a
setCohesionMod :: LensModality a => LensSet Cohesion a
mapCohesionMod :: LensModality a => LensMap Cohesion a
data Q0Origin
- = Q0Inferred
- | Q0 Range
- | Q0Erased Range
data Q1Origin
- = Q1Inferred
- | Q1 Range
- | Q1Linear Range
data QωOrigin
- = QωInferred
- | Qω Range
- | QωPlenty Range
data Quantity
- = Quantity0 Q0Origin
- | Quantity1 Q1Origin
- | Quantityω QωOrigin
defaultQuantity :: Quantity
sameQuantity :: Quantity -> Quantity -> Bool
addQuantity :: Quantity -> Quantity -> Quantity
zeroQuantity :: Quantity
topQuantity :: Quantity
moreQuantity :: Quantity -> Quantity -> Bool
composeQuantity :: Quantity -> Quantity -> Quantity
applyQuantity :: LensQuantity a => Quantity -> a -> a
inverseComposeQuantity :: Quantity -> Quantity -> Quantity
inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a
hasQuantity0 :: LensQuantity a => a -> Bool
hasQuantity1 :: LensQuantity a => a -> Bool
hasQuantityω :: LensQuantity a => a -> Bool
noUserQuantity :: LensQuantity a => a -> Bool
usableQuantity :: LensQuantity a => a -> Bool
class LensQuantity a where
- getQuantity :: a -> Quantity
- setQuantity :: Quantity -> a -> a
- mapQuantity :: (Quantity -> Quantity) -> a -> a
data Relevance
- = 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
sameRelevance :: Relevance -> Relevance -> Bool
usableRelevance :: LensRelevance a => a -> Bool
composeRelevance :: Relevance -> Relevance -> Relevance
applyRelevance :: LensRelevance a => Relevance -> a -> a
inverseComposeRelevance :: Relevance -> Relevance -> Relevance
inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a
addRelevance :: Relevance -> Relevance -> Relevance
zeroRelevance :: Relevance
topRelevance :: Relevance
irrToNonStrict :: Relevance -> Relevance
nonStrictToRel :: Relevance -> Relevance
nonStrictToIrr :: Relevance -> Relevance
data Cohesion
- = Flat
- | Continuous
- | Squash
allCohesions :: [Cohesion]
defaultCohesion :: Cohesion
class LensCohesion a where
- getCohesion :: a -> Cohesion
- setCohesion :: Cohesion -> a -> a
- mapCohesion :: (Cohesion -> Cohesion) -> a -> a
moreCohesion :: Cohesion -> Cohesion -> Bool
sameCohesion :: Cohesion -> Cohesion -> Bool
usableCohesion :: LensCohesion a => a -> Bool
composeCohesion :: Cohesion -> Cohesion -> Cohesion
applyCohesion :: LensCohesion a => Cohesion -> a -> a
inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion
inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a
addCohesion :: Cohesion -> Cohesion -> Cohesion
zeroCohesion :: Cohesion
topCohesion :: Cohesion
data Origin
- = 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
isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool
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 Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
}
type Named_ = Named NamedName
type NamedName = WithOrigin (Ranged ArgName)
sameName :: NamedName -> NamedName -> Bool
unnamed :: a -> Named name a
named :: name -> a -> Named name a
userNamed :: Ranged ArgName -> a -> Named_ a
class LensNamed name a | a -> name where
- 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
bareNameOf :: LensNamed NamedName a => a -> Maybe ArgName
bareNameWithDefault :: LensNamed NamedName a => ArgName -> a -> ArgName
namedSame :: (LensNamed NamedName a, LensNamed NamedName b) => a -> b -> Bool
fittingNamedArg :: (LensNamed NamedName arg, LensHiding arg, LensNamed NamedName dom, LensHiding dom) => arg -> dom -> Maybe Bool
type NamedArg a = Arg (Named_ a)
namedArg :: NamedArg a -> a
defaultNamedArg :: a -> NamedArg a
unnamedArg :: ArgInfo -> a -> NamedArg a
updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b)
setNamedArg :: NamedArg a -> b -> NamedArg b
type ArgName = String
argNameToString :: ArgName -> String
stringToArgName :: String -> ArgName
appendArgNames :: ArgName -> ArgName -> ArgName
data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
}
unranged :: a -> Ranged a
type RawName = String
rawNameToString :: RawName -> String
stringToRawName :: String -> RawName
type RString = Ranged RawName
data ConOrigin
- = 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
data IsAbstract
- = AbstractDef
- | ConcreteDef
class LensIsAbstract a where
- lensIsAbstract :: Lens' IsAbstract a
class AnyIsAbstract a where
- anyIsAbstract :: a -> IsAbstract
data IsInstance
- = InstanceDef Range
- | NotInstanceDef
data IsMacro
- = MacroDef
- | NotMacroDef
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
}
type PrecedenceLevel = Double
data FixityLevel
- = Unrelated
- | Related !PrecedenceLevel
data Associativity
- = NonAssoc
- | LeftAssoc
- | RightAssoc
data Fixity = Fixity {
- fixityRange :: Range
- fixityLevel :: !FixityLevel
- fixityAssoc :: !Associativity
}
noFixity :: Fixity
defaultFixity :: Fixity
data Fixity' = Fixity' {
- theFixity :: !Fixity
- theNotation :: Notation
- theNameRange :: Range
}
noFixity' :: Fixity'
_fixityAssoc :: Lens' Associativity Fixity
_fixityLevel :: Lens' FixityLevel Fixity
class LensFixity a where
- lensFixity :: Lens' Fixity a
class LensFixity' a where
- lensFixity' :: Lens' Fixity' a
data ImportDirective' n m = ImportDirective {
- importDirRange :: Range
- using :: Using' n m
- hiding :: [ImportedName' n m]
- impRenaming :: [Renaming' n m]
- publicOpen :: Maybe Range
}
defaultImportDir :: ImportDirective' n m
isDefaultImportDir :: ImportDirective' n m -> Bool
data Using' n m
- = UseEverything
- | Using [ImportedName' n m]
mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2
data ImportedName' n m
- = ImportedModule m
- | ImportedName n
setImportedName :: ImportedName' a a -> a -> ImportedName' a a
data Renaming' n m = Renaming {
- renFrom :: ImportedName' n m
- renTo :: ImportedName' n m
- renFixity :: Maybe Fixity
- renToRange :: Range
}
data TerminationCheck m
- = TerminationCheck
- | NoTerminationCheck
- | NonTerminating
- | Terminating
- | TerminationMeasure Range m
data PositivityCheck
- = YesPositivityCheck
- | NoPositivityCheck
data UniverseCheck
- = YesUniverseCheck
- | NoUniverseCheck
data CoverageCheck
- = YesCoverageCheck
- | NoCoverageCheck
data RewriteEqn' qn p e
- = Rewrite [(qn, e)]
- | Invert qn [(p, e)]
data ExpandedEllipsis
- = ExpandedEllipsis {
  - ellipsisRange :: Range
  - ellipsisWithArgs :: Int
  }
- | NoEllipsis
type Notation = [GenPart]
noNotation :: Notation
data GenPart
- = BindHole Range (Ranged Int)
- | NormalHole Range (NamedArg (Ranged Int))
- | WildHole (Ranged Int)
- | IdPart RString

Documentation

type Nat = Int Source #

type Arity = Nat Source #

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 # (/=) :: Delayed -> Delayed -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Delayed # toConstr :: Delayed -> Constr # dataTypeOf :: Delayed -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Delayed) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Delayed) # gmapT :: (forall b. Data b => b -> b) -> Delayed -> Delayed # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r # gmapQ :: (forall d. Data d => d -> u) -> Delayed -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Delayed -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed #
Ord Delayed Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Delayed -> Delayed -> Ordering # (<) :: Delayed -> Delayed -> Bool # (<=) :: Delayed -> Delayed -> Bool # (>) :: Delayed -> Delayed -> Bool # (>=) :: Delayed -> Delayed -> Bool # max :: Delayed -> Delayed -> Delayed # min :: Delayed -> Delayed -> Delayed #
Show Delayed Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Delayed -> ShowS # show :: Delayed -> String # showList :: [Delayed] -> ShowS #
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 # (/=) :: FileType -> FileType -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FileType # toConstr :: FileType -> Constr # dataTypeOf :: FileType -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FileType) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FileType) # gmapT :: (forall b. Data b => b -> b) -> FileType -> FileType # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FileType -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FileType -> r # gmapQ :: (forall d. Data d => d -> u) -> FileType -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FileType -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FileType -> m FileType # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FileType -> m FileType # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FileType -> m FileType #
Ord FileType Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: FileType -> FileType -> Ordering # (<) :: FileType -> FileType -> Bool # (<=) :: FileType -> FileType -> Bool # (>) :: FileType -> FileType -> Bool # (>=) :: FileType -> FileType -> Bool # max :: FileType -> FileType -> FileType # min :: FileType -> FileType -> FileType #
Show FileType Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> FileType -> ShowS # show :: FileType -> String # showList :: [FileType] -> ShowS #
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 # (/=) :: HasEta -> HasEta -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HasEta # toConstr :: HasEta -> Constr # dataTypeOf :: HasEta -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HasEta) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HasEta) # gmapT :: (forall b. Data b => b -> b) -> HasEta -> HasEta # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HasEta -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HasEta -> r # gmapQ :: (forall d. Data d => d -> u) -> HasEta -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HasEta -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta #
Ord HasEta Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: HasEta -> HasEta -> Ordering # (<) :: HasEta -> HasEta -> Bool # (<=) :: HasEta -> HasEta -> Bool # (>) :: HasEta -> HasEta -> Bool # (>=) :: HasEta -> HasEta -> Bool # max :: HasEta -> HasEta -> HasEta # min :: HasEta -> HasEta -> HasEta #
Show HasEta Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> HasEta -> ShowS # show :: HasEta -> String # showList :: [HasEta] -> ShowS #
NFData HasEta Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: HasEta -> () #
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 # (/=) :: Induction -> Induction -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Induction # toConstr :: Induction -> Constr # dataTypeOf :: Induction -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Induction) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Induction) # gmapT :: (forall b. Data b => b -> b) -> Induction -> Induction # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r # gmapQ :: (forall d. Data d => d -> u) -> Induction -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Induction -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Induction -> m Induction # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction #
Ord Induction Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Induction -> Induction -> Ordering # (<) :: Induction -> Induction -> Bool # (<=) :: Induction -> Induction -> Bool # (>) :: Induction -> Induction -> Bool # (>=) :: Induction -> Induction -> Bool # max :: Induction -> Induction -> Induction # min :: Induction -> Induction -> Induction #
Show Induction Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Induction -> ShowS # show :: Induction -> String # showList :: [Induction] -> ShowS #
NFData Induction Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Induction -> () #
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 # (/=) :: Overlappable -> Overlappable -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Overlappable # toConstr :: Overlappable -> Constr # dataTypeOf :: Overlappable -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Overlappable) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Overlappable) # gmapT :: (forall b. Data b => b -> b) -> Overlappable -> Overlappable # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Overlappable -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Overlappable -> r # gmapQ :: (forall d. Data d => d -> u) -> Overlappable -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Overlappable -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Overlappable -> m Overlappable #
Ord Overlappable Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Overlappable -> Overlappable -> Ordering # (<) :: Overlappable -> Overlappable -> Bool # (<=) :: Overlappable -> Overlappable -> Bool # (>) :: Overlappable -> Overlappable -> Bool # (>=) :: Overlappable -> Overlappable -> Bool # max :: Overlappable -> Overlappable -> Overlappable # min :: Overlappable -> Overlappable -> Overlappable #
Show Overlappable Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Overlappable -> ShowS # show :: Overlappable -> String # showList :: [Overlappable] -> ShowS #
Semigroup Overlappable Source #	Just for the `Hiding` instance. Should never combine different overlapping.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Overlappable -> Overlappable -> Overlappable # sconcat :: NonEmpty Overlappable -> Overlappable # stimes :: Integral b => b -> Overlappable -> Overlappable #
Monoid Overlappable Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: Overlappable # mappend :: Overlappable -> Overlappable -> Overlappable # mconcat :: [Overlappable] -> Overlappable #
NFData Overlappable Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Overlappable -> () #

data Hiding Source #

Constructors

Hidden
Instance Overlappable
NotHidden

Instances

Eq Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Hiding -> Hiding -> Bool # (/=) :: Hiding -> Hiding -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Hiding # toConstr :: Hiding -> Constr # dataTypeOf :: Hiding -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Hiding) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Hiding) # gmapT :: (forall b. Data b => b -> b) -> Hiding -> Hiding # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r # gmapQ :: (forall d. Data d => d -> u) -> Hiding -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Hiding -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding #
Ord Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Hiding -> Hiding -> Ordering # (<) :: Hiding -> Hiding -> Bool # (<=) :: Hiding -> Hiding -> Bool # (>) :: Hiding -> Hiding -> Bool # (>=) :: Hiding -> Hiding -> Bool # max :: Hiding -> Hiding -> Hiding # min :: Hiding -> Hiding -> Hiding #
Show Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Hiding -> ShowS # show :: Hiding -> String # showList :: [Hiding] -> ShowS #
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 # sconcat :: NonEmpty Hiding -> Hiding # stimes :: Integral b => b -> Hiding -> Hiding #
Monoid Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: Hiding # mappend :: Hiding -> Hiding -> Hiding # mconcat :: [Hiding] -> Hiding #
NFData Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Hiding -> () #
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 # (<$) :: a -> WithHiding b -> WithHiding a #
Applicative WithHiding Source #
Instance details Defined in Agda.Syntax.Common Methods pure :: a -> WithHiding a # (<>) :: WithHiding (a -> b) -> WithHiding a -> WithHiding b # liftA2 :: (a -> b -> c) -> WithHiding a -> WithHiding b -> WithHiding c # (>) :: WithHiding a -> WithHiding b -> WithHiding b # (<*) :: WithHiding a -> WithHiding b -> WithHiding a #
Foldable WithHiding Source #
Instance details Defined in Agda.Syntax.Common Methods fold :: Monoid m => WithHiding m -> m # foldMap :: Monoid m => (a -> m) -> WithHiding a -> m # foldr :: (a -> b -> b) -> b -> WithHiding a -> b # foldr' :: (a -> b -> b) -> b -> WithHiding a -> b # foldl :: (b -> a -> b) -> b -> WithHiding a -> b # foldl' :: (b -> a -> b) -> b -> WithHiding a -> b # foldr1 :: (a -> a -> a) -> WithHiding a -> a # foldl1 :: (a -> a -> a) -> WithHiding a -> a # toList :: WithHiding a -> [a] # null :: WithHiding a -> Bool # length :: WithHiding a -> Int # elem :: Eq a => a -> WithHiding a -> Bool # maximum :: Ord a => WithHiding a -> a # minimum :: Ord a => WithHiding a -> a # sum :: Num a => WithHiding a -> a # product :: Num a => WithHiding a -> a #
Traversable WithHiding Source #
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> WithHiding a -> f (WithHiding b) # sequenceA :: Applicative f => WithHiding (f a) -> f (WithHiding a) # mapM :: Monad m => (a -> m b) -> WithHiding a -> m (WithHiding b) # sequence :: Monad m => WithHiding (m a) -> m (WithHiding a) #
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 #
Subst t a => Subst t (WithHiding a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> WithHiding a -> WithHiding a Source #
ToConcrete RHS (RHS, [RewriteEqn], [WithHiding Expr], [Declaration]) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [RewriteEqn], [WithHiding Expr], [Declaration]) Source # bindToConcrete :: RHS -> ((RHS0, [RewriteEqn], [WithHiding Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b Source #
Eq a => Eq (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: WithHiding a -> WithHiding a -> Bool # (/=) :: WithHiding a -> WithHiding a -> Bool #
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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WithHiding a) # toConstr :: WithHiding a -> Constr # dataTypeOf :: WithHiding a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WithHiding a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WithHiding a)) # gmapT :: (forall b. Data b => b -> b) -> WithHiding a -> WithHiding a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithHiding a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithHiding a -> r # gmapQ :: (forall d. Data d => d -> u) -> WithHiding a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> WithHiding a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithHiding a -> m (WithHiding a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithHiding a -> m (WithHiding a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithHiding a -> m (WithHiding a) #
Ord a => Ord (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: WithHiding a -> WithHiding a -> Ordering # (<) :: WithHiding a -> WithHiding a -> Bool # (<=) :: WithHiding a -> WithHiding a -> Bool # (>) :: WithHiding a -> WithHiding a -> Bool # (>=) :: WithHiding a -> WithHiding a -> Bool # max :: WithHiding a -> WithHiding a -> WithHiding a # min :: WithHiding a -> WithHiding a -> WithHiding a #
Show a => Show (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> WithHiding a -> ShowS # show :: WithHiding a -> String # showList :: [WithHiding a] -> ShowS #
NFData a => NFData (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: WithHiding a -> () #
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 #
ExprLike a => ExprLike (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WithHiding a -> m (WithHiding a) Source # foldExpr :: Monoid m => (Expr -> m) -> WithHiding a -> m Source #
Free t => Free (WithHiding t) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => WithHiding t -> FreeM a c Source #
TermLike a => TermLike (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> WithHiding a -> m (WithHiding a) Source # foldTerm :: Monoid m => (Term -> m) -> WithHiding a -> m Source #
ExprLike a => ExprLike (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> WithHiding a -> m (WithHiding a) Source # foldExpr :: Monoid m => (Expr -> m) -> WithHiding a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> WithHiding a -> m (WithHiding a) Source # mapExpr :: (Expr -> Expr) -> 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 :: MonadPretty m => WithHiding a -> m Doc Source #
Normalise t => Normalise (WithHiding t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: WithHiding t -> ReduceM (WithHiding t) 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 :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m 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 mapHiding or LensArgInfo.

Minimal complete definition

Nothing

Methods

getHiding :: a -> Hiding Source #

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

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

getHiding :: LensArgInfo a => a -> Hiding Source #

mapHiding :: LensArgInfo a => (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 (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 #
LensHiding (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getHiding :: Dom' t e -> Hiding Source # setHiding :: Hiding -> Dom' t e -> Dom' t e Source # mapHiding :: (Hiding -> Hiding) -> Dom' t e -> Dom' t e 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.
modCohesion :: Cohesion
Cohesion/what was in Agda-flat. see "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" (arXiv:1509.07584) Currently only the comonad is implemented.

Instances

Eq Modality Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Modality -> Modality -> Bool # (/=) :: Modality -> Modality -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Modality # toConstr :: Modality -> Constr # dataTypeOf :: Modality -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Modality) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Modality) # gmapT :: (forall b. Data b => b -> b) -> Modality -> Modality # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Modality -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Modality -> r # gmapQ :: (forall d. Data d => d -> u) -> Modality -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Modality -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Modality -> m Modality # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Modality -> m Modality # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Modality -> m Modality #
Ord Modality Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Modality -> Modality -> Ordering # (<) :: Modality -> Modality -> Bool # (<=) :: Modality -> Modality -> Bool # (>) :: Modality -> Modality -> Bool # (>=) :: Modality -> Modality -> Bool # max :: Modality -> Modality -> Modality # min :: Modality -> Modality -> Modality #
Show Modality Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Modality -> ShowS # show :: Modality -> String # showList :: [Modality] -> ShowS #
Generic Modality Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Modality :: Type -> Type # Methods from :: Modality -> Rep Modality x # to :: Rep Modality x -> Modality #
Semigroup Modality Source #	Pointwise composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Modality -> Modality -> Modality # sconcat :: NonEmpty Modality -> Modality # stimes :: Integral b => b -> Modality -> Modality #
Monoid Modality Source #	Pointwise unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: Modality # mappend :: Modality -> Modality -> Modality # mconcat :: [Modality] -> Modality #
NFData Modality Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Modality -> () #
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 #
LensCohesion Modality Source #
Instance details Defined in Agda.Syntax.Common Methods getCohesion :: Modality -> Cohesion Source # setCohesion :: Cohesion -> Modality -> Modality Source # mapCohesion :: (Cohesion -> Cohesion) -> Modality -> 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 #
PrettyTCM Modality Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Modality -> m Doc Source #
Unquote Modality Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Modality Source #
IsVarSet () AllowedVar Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar Source #
type Rep Modality Source #
Instance details Defined in Agda.Syntax.Common type Rep Modality = D1 (MetaData "Modality" "Agda.Syntax.Common" "Agda-2.6.1-HTVbJ7KJ8pbJE1PvbUqEEQ" False) (C1 (MetaCons "Modality" PrefixI True) (S1 (MetaSel (Just "modRelevance") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Relevance) :: (S1 (MetaSel (Just "modQuantity") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Quantity) :: S1 (MetaSel (Just "modCohesion") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Cohesion))))

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 #

Multiplicative monoid (standard monoid).

applyModality :: LensModality a => Modality -> a -> a Source #

Compose with modality flag from the left. This function is e.g. used to update the modality information on pattern variables a after a match against something of modality q.

inverseComposeModality :: Modality -> Modality -> Modality Source #

inverseComposeModality r x returns the least modality y such that forall x, y we have x `moreUsableModality` (r `composeModality` y) iff (r `inverseComposeModality` x) `moreUsableModality` y (Galois connection).

inverseApplyModality :: LensModality a => Modality -> a -> a Source #

Left division by a Modality. Used e.g. to modify context when going into a m argument.

addModality :: Modality -> Modality -> Modality Source #

Modality forms a pointwise additive monoid.

zeroModality :: Modality Source #

topModality :: Modality Source #

Absorptive element under addition.

sameModality :: (LensModality a, LensModality b) => a -> b -> Bool Source #

Equality ignoring origin.

lModRelevance :: Lens' Relevance Modality Source #

lModQuantity :: Lens' Quantity Modality Source #

lModCohesion :: Lens' Cohesion Modality Source #

class LensModality a where Source #

Minimal complete definition

Nothing

Methods

getModality :: a -> Modality Source #

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

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

getModality :: LensArgInfo a => a -> Modality Source #

mapModality :: LensArgInfo a => (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 TCEnv Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getModality :: TCEnv -> Modality Source # setModality :: Modality -> TCEnv -> TCEnv Source # mapModality :: (Modality -> Modality) -> TCEnv -> TCEnv Source #
LensModality Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getModality :: Definition -> Modality Source # setModality :: Modality -> Definition -> Definition Source # mapModality :: (Modality -> Modality) -> Definition -> Definition 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 #
LensModality (VarOcc' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getModality :: VarOcc' a -> Modality Source # setModality :: Modality -> VarOcc' a -> VarOcc' a Source # mapModality :: (Modality -> Modality) -> VarOcc' a -> VarOcc' a Source #
LensModality (FlexibleVar a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getModality :: FlexibleVar a -> Modality Source # setModality :: Modality -> FlexibleVar a -> FlexibleVar a Source # mapModality :: (Modality -> Modality) -> FlexibleVar a -> FlexibleVar a Source #
LensModality (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getModality :: Dom' t e -> Modality Source # setModality :: Modality -> Dom' t e -> Dom' t e Source # mapModality :: (Modality -> Modality) -> Dom' t e -> Dom' t e Source #
LensModality (FreeEnv' a b c) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getModality :: FreeEnv' a b c -> Modality Source # setModality :: Modality -> FreeEnv' a b c -> FreeEnv' a b c Source # mapModality :: (Modality -> Modality) -> FreeEnv' a b c -> FreeEnv' a b c 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 #

getCohesionMod :: LensModality a => LensGet Cohesion a Source #

setCohesionMod :: LensModality a => LensSet Cohesion a Source #

mapCohesionMod :: LensModality a => LensMap Cohesion a Source #

Quantities

Quantity origin.

data Q0Origin Source #

Origin of Quantity0.

Constructors

Q0Inferred	User wrote nothing.
Q0 Range	User wrote "@0".
Q0Erased Range	User wrote "@erased".

Instances

Eq Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Q0Origin -> Q0Origin -> Bool # (/=) :: Q0Origin -> Q0Origin -> Bool #
Data Q0Origin 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) -> Q0Origin -> c Q0Origin # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Q0Origin # toConstr :: Q0Origin -> Constr # dataTypeOf :: Q0Origin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Q0Origin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q0Origin) # gmapT :: (forall b. Data b => b -> b) -> Q0Origin -> Q0Origin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q0Origin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q0Origin -> r # gmapQ :: (forall d. Data d => d -> u) -> Q0Origin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Q0Origin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Q0Origin -> m Q0Origin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Q0Origin -> m Q0Origin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Q0Origin -> m Q0Origin #
Ord Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Q0Origin -> Q0Origin -> Ordering # (<) :: Q0Origin -> Q0Origin -> Bool # (<=) :: Q0Origin -> Q0Origin -> Bool # (>) :: Q0Origin -> Q0Origin -> Bool # (>=) :: Q0Origin -> Q0Origin -> Bool # max :: Q0Origin -> Q0Origin -> Q0Origin # min :: Q0Origin -> Q0Origin -> Q0Origin #
Show Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Q0Origin -> ShowS # show :: Q0Origin -> String # showList :: [Q0Origin] -> ShowS #
Generic Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Q0Origin :: Type -> Type # Methods from :: Q0Origin -> Rep Q0Origin x # to :: Rep Q0Origin x -> Q0Origin #
Semigroup Q0Origin Source #	Right-biased composition, because the left quantity acts as context, and the right one as occurrence.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Q0Origin -> Q0Origin -> Q0Origin # sconcat :: NonEmpty Q0Origin -> Q0Origin # stimes :: Integral b => b -> Q0Origin -> Q0Origin #
Monoid Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: Q0Origin # mappend :: Q0Origin -> Q0Origin -> Q0Origin # mconcat :: [Q0Origin] -> Q0Origin #
NFData Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Q0Origin -> () #
Null Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Q0Origin Source # null :: Q0Origin -> Bool Source #
Pretty Q0Origin Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Q0Origin -> Doc Source # prettyPrec :: Int -> Q0Origin -> Doc Source # prettyList :: [Q0Origin] -> Doc Source #
KillRange Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Q0Origin Source #
SetRange Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Q0Origin -> Q0Origin Source #
HasRange Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Q0Origin -> Range Source #
EmbPrj Q0Origin Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Q0Origin -> S Int32 Source # icod_ :: Q0Origin -> S Int32 Source # value :: Int32 -> R Q0Origin Source #
type Rep Q0Origin Source #
Instance details Defined in Agda.Syntax.Common type Rep Q0Origin = D1 (MetaData "Q0Origin" "Agda.Syntax.Common" "Agda-2.6.1-HTVbJ7KJ8pbJE1PvbUqEEQ" False) (C1 (MetaCons "Q0Inferred" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Q0" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range)) :+: C1 (MetaCons "Q0Erased" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range))))

data Q1Origin Source #

Origin of Quantity1.

Constructors

Q1Inferred	User wrote nothing.
Q1 Range	User wrote "@1".
Q1Linear Range	User wrote "@linear".

Instances

Eq Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Q1Origin -> Q1Origin -> Bool # (/=) :: Q1Origin -> Q1Origin -> Bool #
Data Q1Origin 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) -> Q1Origin -> c Q1Origin # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Q1Origin # toConstr :: Q1Origin -> Constr # dataTypeOf :: Q1Origin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Q1Origin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Q1Origin) # gmapT :: (forall b. Data b => b -> b) -> Q1Origin -> Q1Origin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Q1Origin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Q1Origin -> r # gmapQ :: (forall d. Data d => d -> u) -> Q1Origin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Q1Origin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Q1Origin -> m Q1Origin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Q1Origin -> m Q1Origin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Q1Origin -> m Q1Origin #
Ord Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Q1Origin -> Q1Origin -> Ordering # (<) :: Q1Origin -> Q1Origin -> Bool # (<=) :: Q1Origin -> Q1Origin -> Bool # (>) :: Q1Origin -> Q1Origin -> Bool # (>=) :: Q1Origin -> Q1Origin -> Bool # max :: Q1Origin -> Q1Origin -> Q1Origin # min :: Q1Origin -> Q1Origin -> Q1Origin #
Show Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Q1Origin -> ShowS # show :: Q1Origin -> String # showList :: [Q1Origin] -> ShowS #
Generic Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Q1Origin :: Type -> Type # Methods from :: Q1Origin -> Rep Q1Origin x # to :: Rep Q1Origin x -> Q1Origin #
Semigroup Q1Origin Source #	Right-biased composition, because the left quantity acts as context, and the right one as occurrence.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Q1Origin -> Q1Origin -> Q1Origin # sconcat :: NonEmpty Q1Origin -> Q1Origin # stimes :: Integral b => b -> Q1Origin -> Q1Origin #
Monoid Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: Q1Origin # mappend :: Q1Origin -> Q1Origin -> Q1Origin # mconcat :: [Q1Origin] -> Q1Origin #
NFData Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Q1Origin -> () #
Null Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Q1Origin Source # null :: Q1Origin -> Bool Source #
Pretty Q1Origin Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Q1Origin -> Doc Source # prettyPrec :: Int -> Q1Origin -> Doc Source # prettyList :: [Q1Origin] -> Doc Source #
KillRange Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Q1Origin Source #
SetRange Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Q1Origin -> Q1Origin Source #
HasRange Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Q1Origin -> Range Source #
EmbPrj Q1Origin Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Q1Origin -> S Int32 Source # icod_ :: Q1Origin -> S Int32 Source # value :: Int32 -> R Q1Origin Source #
type Rep Q1Origin Source #
Instance details Defined in Agda.Syntax.Common type Rep Q1Origin = D1 (MetaData "Q1Origin" "Agda.Syntax.Common" "Agda-2.6.1-HTVbJ7KJ8pbJE1PvbUqEEQ" False) (C1 (MetaCons "Q1Inferred" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Q1" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range)) :+: C1 (MetaCons "Q1Linear" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range))))

data QωOrigin Source #

Origin of Quantityω.

Constructors

QωInferred	User wrote nothing.
Qω Range	User wrote "@ω".
QωPlenty Range	User wrote "@plenty".

Instances

Eq QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: QωOrigin -> QωOrigin -> Bool # (/=) :: QωOrigin -> QωOrigin -> Bool #
Data Qω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) -> QωOrigin -> c QωOrigin # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QωOrigin # toConstr :: QωOrigin -> Constr # dataTypeOf :: QωOrigin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QωOrigin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QωOrigin) # gmapT :: (forall b. Data b => b -> b) -> QωOrigin -> QωOrigin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QωOrigin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QωOrigin -> r # gmapQ :: (forall d. Data d => d -> u) -> QωOrigin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> QωOrigin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> QωOrigin -> m QωOrigin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QωOrigin -> m QωOrigin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QωOrigin -> m QωOrigin #
Ord QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: QωOrigin -> QωOrigin -> Ordering # (<) :: QωOrigin -> QωOrigin -> Bool # (<=) :: QωOrigin -> QωOrigin -> Bool # (>) :: QωOrigin -> QωOrigin -> Bool # (>=) :: QωOrigin -> QωOrigin -> Bool # max :: QωOrigin -> QωOrigin -> QωOrigin # min :: QωOrigin -> QωOrigin -> QωOrigin #
Show QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> QωOrigin -> ShowS # show :: QωOrigin -> String # showList :: [QωOrigin] -> ShowS #
Generic QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep QωOrigin :: Type -> Type # Methods from :: QωOrigin -> Rep QωOrigin x # to :: Rep QωOrigin x -> QωOrigin #
Semigroup QωOrigin Source #	Right-biased composition, because the left quantity acts as context, and the right one as occurrence.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: QωOrigin -> QωOrigin -> QωOrigin # sconcat :: NonEmpty QωOrigin -> QωOrigin # stimes :: Integral b => b -> QωOrigin -> QωOrigin #
Monoid QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: QωOrigin # mappend :: QωOrigin -> QωOrigin -> QωOrigin # mconcat :: [QωOrigin] -> QωOrigin #
NFData QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: QωOrigin -> () #
Null QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: QωOrigin Source # null :: QωOrigin -> Bool Source #
Pretty QωOrigin Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: QωOrigin -> Doc Source # prettyPrec :: Int -> QωOrigin -> Doc Source # prettyList :: [QωOrigin] -> Doc Source #
KillRange QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT QωOrigin Source #
SetRange QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> QωOrigin -> QωOrigin Source #
HasRange QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: QωOrigin -> Range Source #
EmbPrj QωOrigin Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: QωOrigin -> S Int32 Source # icod_ :: QωOrigin -> S Int32 Source # value :: Int32 -> R QωOrigin Source #
type Rep QωOrigin Source #
Instance details Defined in Agda.Syntax.Common type Rep QωOrigin = D1 (MetaData "Q\969Origin" "Agda.Syntax.Common" "Agda-2.6.1-HTVbJ7KJ8pbJE1PvbUqEEQ" False) (C1 (MetaCons "Q\969Inferred" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Q\969" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range)) :+: C1 (MetaCons "Q\969Plenty" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range))))

Instances for `Q0Origin`.

Instances for `Q1Origin`.

Instances for `QωOrigin`.

Quantity.

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

Instances

Eq Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Quantity -> Quantity -> Bool # (/=) :: Quantity -> Quantity -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quantity # toConstr :: Quantity -> Constr # dataTypeOf :: Quantity -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quantity) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantity) # gmapT :: (forall b. Data b => b -> b) -> Quantity -> Quantity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r # gmapQ :: (forall d. Data d => d -> u) -> Quantity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Quantity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity #
Ord Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Quantity -> Quantity -> Ordering # (<) :: Quantity -> Quantity -> Bool # (<=) :: Quantity -> Quantity -> Bool # (>) :: Quantity -> Quantity -> Bool # (>=) :: Quantity -> Quantity -> Bool # max :: Quantity -> Quantity -> Quantity # min :: Quantity -> Quantity -> Quantity #
Show Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Quantity -> ShowS # show :: Quantity -> String # showList :: [Quantity] -> ShowS #
Generic Quantity Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Quantity :: Type -> Type # Methods from :: Quantity -> Rep Quantity x # to :: Rep Quantity x -> Quantity #
Semigroup Quantity Source #	Composition of quantities (multiplication). `Quantity0` is dominant. `Quantity1` is neutral. Right-biased for origin.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Quantity -> Quantity -> Quantity # sconcat :: NonEmpty Quantity -> Quantity # stimes :: Integral b => b -> Quantity -> Quantity #
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 # mappend :: Quantity -> Quantity -> Quantity # mconcat :: [Quantity] -> Quantity #
NFData Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Quantity -> () #
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
Pretty Quantity Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Quantity -> Doc Source # prettyPrec :: Int -> Quantity -> Doc Source # prettyList :: [Quantity] -> Doc Source #
KillRange Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Quantity Source #
SetRange Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Quantity -> Quantity Source #
HasRange Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Quantity -> Range 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 #
PrettyTCM Quantity Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Quantity -> m Doc Source #
UniverseBi Declaration Quantity Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [Quantity] #
type Rep Quantity Source #
Instance details Defined in Agda.Syntax.Common type Rep Quantity = D1 (MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.1-HTVbJ7KJ8pbJE1PvbUqEEQ" False) (C1 (MetaCons "Quantity0" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Q0Origin)) :+: (C1 (MetaCons "Quantity1" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Q1Origin)) :+: C1 (MetaCons "Quantity\969" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 QωOrigin))))

defaultQuantity :: Quantity Source #

sameQuantity :: Quantity -> Quantity -> Bool Source #

Equality ignoring origin.

addQuantity :: Quantity -> Quantity -> Quantity Source #

Quantity forms an additive monoid with zero Quantity0.

zeroQuantity :: Quantity Source #

topQuantity :: Quantity Source #

Absorptive element is ω.

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

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

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.

hasQuantity0 :: LensQuantity a => a -> Bool Source #

Check for Quantity0.

hasQuantity1 :: LensQuantity a => a -> Bool Source #

Check for Quantity1.

hasQuantityω :: LensQuantity a => a -> Bool Source #

Check for Quantityω.

noUserQuantity :: LensQuantity a => a -> Bool Source #

Did the user supply a quantity annotation?

usableQuantity :: LensQuantity a => a -> Bool Source #

A thing of quantity 0 is unusable, all others are usable.

class LensQuantity a where Source #

Minimal complete definition

Nothing

Methods

getQuantity :: a -> Quantity Source #

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

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

getQuantity :: LensModality a => a -> Quantity Source #

mapQuantity :: LensModality a => (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 TCEnv Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getQuantity :: TCEnv -> Quantity Source # setQuantity :: Quantity -> TCEnv -> TCEnv Source # mapQuantity :: (Quantity -> Quantity) -> TCEnv -> TCEnv Source #
LensQuantity Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getQuantity :: Definition -> Quantity Source # setQuantity :: Quantity -> Definition -> Definition Source # mapQuantity :: (Quantity -> Quantity) -> Definition -> Definition Source #
LensQuantity (Arg e) Source #
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 #
LensQuantity (VarOcc' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getQuantity :: VarOcc' a -> Quantity Source # setQuantity :: Quantity -> VarOcc' a -> VarOcc' a Source # mapQuantity :: (Quantity -> Quantity) -> VarOcc' a -> VarOcc' a Source #
LensQuantity (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getQuantity :: Dom' t e -> Quantity Source # setQuantity :: Quantity -> Dom' t e -> Dom' t e Source # mapQuantity :: (Quantity -> Quantity) -> Dom' t e -> Dom' t e Source #
LensQuantity (FreeEnv' a b c) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getQuantity :: FreeEnv' a b c -> Quantity Source # setQuantity :: Quantity -> FreeEnv' a b c -> FreeEnv' a b c Source # mapQuantity :: (Quantity -> Quantity) -> FreeEnv' a b c -> FreeEnv' a b c 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 # maxBound :: Relevance #
Enum Relevance Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: Relevance -> Relevance # pred :: Relevance -> Relevance # toEnum :: Int -> Relevance # fromEnum :: Relevance -> Int # enumFrom :: Relevance -> [Relevance] # enumFromThen :: Relevance -> Relevance -> [Relevance] # enumFromTo :: Relevance -> Relevance -> [Relevance] # enumFromThenTo :: Relevance -> Relevance -> Relevance -> [Relevance] #
Eq Relevance Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Relevance -> Relevance -> Bool # (/=) :: Relevance -> Relevance -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Relevance # toConstr :: Relevance -> Constr # dataTypeOf :: Relevance -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Relevance) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Relevance) # gmapT :: (forall b. Data b => b -> b) -> Relevance -> Relevance # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Relevance -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Relevance -> r # gmapQ :: (forall d. Data d => d -> u) -> Relevance -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Relevance -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Relevance -> m Relevance #
Ord Relevance Source #	More relevant is smaller.
Instance details Defined in Agda.Syntax.Common Methods compare :: Relevance -> Relevance -> Ordering # (<) :: Relevance -> Relevance -> Bool # (<=) :: Relevance -> Relevance -> Bool # (>) :: Relevance -> Relevance -> Bool # (>=) :: Relevance -> Relevance -> Bool # max :: Relevance -> Relevance -> Relevance # min :: Relevance -> Relevance -> Relevance #
Show Relevance Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Relevance -> ShowS # show :: Relevance -> String # showList :: [Relevance] -> ShowS #
Generic Relevance Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Relevance :: Type -> Type # Methods from :: Relevance -> Rep Relevance x # to :: Rep Relevance x -> Relevance #
Semigroup Relevance Source #	`Relevance` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Relevance -> Relevance -> Relevance # sconcat :: NonEmpty Relevance -> Relevance # stimes :: Integral b => b -> Relevance -> Relevance #
Monoid Relevance Source #	`Relevant` is the unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: Relevance # mappend :: Relevance -> Relevance -> Relevance # mconcat :: [Relevance] -> Relevance #
NFData Relevance Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Relevance -> () #
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 #
SetRange Relevance Source #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Relevance -> Relevance Source #
HasRange Relevance Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Relevance -> Range 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 :: MonadPretty m => Relevance -> m 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.1-HTVbJ7KJ8pbJE1PvbUqEEQ" 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 mapRelevance or LensModality.

Minimal complete definition

Nothing

Methods

getRelevance :: a -> Relevance Source #

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

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

getRelevance :: LensModality a => a -> Relevance Source #

mapRelevance :: LensModality a => (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 TCEnv Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRelevance :: TCEnv -> Relevance Source # setRelevance :: Relevance -> TCEnv -> TCEnv Source # mapRelevance :: (Relevance -> Relevance) -> TCEnv -> TCEnv 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 Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRelevance :: Definition -> Relevance Source # setRelevance :: Relevance -> Definition -> Definition Source # mapRelevance :: (Relevance -> Relevance) -> Definition -> Definition 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 #
LensRelevance (VarOcc' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getRelevance :: VarOcc' a -> Relevance Source # setRelevance :: Relevance -> VarOcc' a -> VarOcc' a Source # mapRelevance :: (Relevance -> Relevance) -> VarOcc' a -> VarOcc' a Source #
LensRelevance (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getRelevance :: Dom' t e -> Relevance Source # setRelevance :: Relevance -> Dom' t e -> Dom' t e Source # mapRelevance :: (Relevance -> Relevance) -> Dom' t e -> Dom' t e Source #
LensRelevance (FreeEnv' a b c) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getRelevance :: FreeEnv' a b c -> Relevance Source # setRelevance :: Relevance -> FreeEnv' a b c -> FreeEnv' a b c Source # mapRelevance :: (Relevance -> Relevance) -> FreeEnv' a b c -> FreeEnv' a b c 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

sameRelevance :: Relevance -> Relevance -> Bool Source #

Equality ignoring origin.

usableRelevance :: LensRelevance a => a -> Bool Source #

usableRelevance rel == False iff we cannot use a variable of rel.

composeRelevance :: Relevance -> Relevance -> Relevance Source #

Relevance composition. Irrelevant is dominant, Relevant is neutral. Composition coincides with max.

applyRelevance :: LensRelevance a => Relevance -> a -> a Source #

Compose with relevance flag from the left. This function is e.g. used to update the relevance information on pattern variables a after a match against something rel.

inverseComposeRelevance :: Relevance -> Relevance -> Relevance Source #

inverseComposeRelevance r x returns the most irrelevant y such that forall x, y we have x `moreRelevant` (r `composeRelevance` y) iff (r `inverseComposeRelevance` x) `moreRelevant` y (Galois connection).

inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a Source #

Left division by a Relevance. Used e.g. to modify context when going into a rel argument.

addRelevance :: Relevance -> Relevance -> Relevance Source #

Combine inferred Relevance. The unit is Irrelevant.

zeroRelevance :: Relevance Source #

Relevance forms a monoid under addition, and even a semiring.

topRelevance :: Relevance Source #

Absorptive element under addition.

irrToNonStrict :: Relevance -> Relevance Source #

Irrelevant function arguments may appear non-strictly in the codomain type.

nonStrictToRel :: Relevance -> Relevance Source #

Applied when working on types (unless --experimental-irrelevance).

nonStrictToIrr :: Relevance -> Relevance Source #

Cohesion

data Cohesion Source #

Cohesion modalities see "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" (arXiv:1509.07584) types are now given an additional topological layer which the modalities interact with.

Constructors

Flat	same points, discrete topology, idempotent comonad, box-like.
Continuous	identity modality. \| Sharp -- ^ same points, codiscrete topology, idempotent monad, diamond-like.
Squash	single point space, artificially added for Flat left-composition.

Instances

Bounded Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods minBound :: Cohesion # maxBound :: Cohesion #
Enum Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: Cohesion -> Cohesion # pred :: Cohesion -> Cohesion # toEnum :: Int -> Cohesion # fromEnum :: Cohesion -> Int # enumFrom :: Cohesion -> [Cohesion] # enumFromThen :: Cohesion -> Cohesion -> [Cohesion] # enumFromTo :: Cohesion -> Cohesion -> [Cohesion] # enumFromThenTo :: Cohesion -> Cohesion -> Cohesion -> [Cohesion] #
Eq Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Cohesion -> Cohesion -> Bool # (/=) :: Cohesion -> Cohesion -> Bool #
Data Cohesion 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) -> Cohesion -> c Cohesion # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Cohesion # toConstr :: Cohesion -> Constr # dataTypeOf :: Cohesion -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Cohesion) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Cohesion) # gmapT :: (forall b. Data b => b -> b) -> Cohesion -> Cohesion # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Cohesion -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Cohesion -> r # gmapQ :: (forall d. Data d => d -> u) -> Cohesion -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Cohesion -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Cohesion -> m Cohesion # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Cohesion -> m Cohesion # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Cohesion -> m Cohesion #
Ord Cohesion Source #	Order is given by implication: flatter is smaller.
Instance details Defined in Agda.Syntax.Common Methods compare :: Cohesion -> Cohesion -> Ordering # (<) :: Cohesion -> Cohesion -> Bool # (<=) :: Cohesion -> Cohesion -> Bool # (>) :: Cohesion -> Cohesion -> Bool # (>=) :: Cohesion -> Cohesion -> Bool # max :: Cohesion -> Cohesion -> Cohesion # min :: Cohesion -> Cohesion -> Cohesion #
Show Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Cohesion -> ShowS # show :: Cohesion -> String # showList :: [Cohesion] -> ShowS #
Generic Cohesion Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Cohesion :: Type -> Type # Methods from :: Cohesion -> Rep Cohesion x # to :: Rep Cohesion x -> Cohesion #
Semigroup Cohesion Source #	`Cohesion` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Cohesion -> Cohesion -> Cohesion # sconcat :: NonEmpty Cohesion -> Cohesion # stimes :: Integral b => b -> Cohesion -> Cohesion #
Monoid Cohesion Source #	`Continous` is the unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: Cohesion # mappend :: Cohesion -> Cohesion -> Cohesion # mconcat :: [Cohesion] -> Cohesion #
NFData Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Cohesion -> () #
PartialOrd Cohesion Source #	Flatter is smaller.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Cohesion Source #
LeftClosedPOMonoid Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: Cohesion -> Cohesion -> Cohesion Source #
POMonoid Cohesion Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup Cohesion Source #
Instance details Defined in Agda.Syntax.Common
Pretty Cohesion Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Cohesion -> Doc Source # prettyPrec :: Int -> Cohesion -> Doc Source # prettyList :: [Cohesion] -> Doc Source #
KillRange Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Cohesion Source #
SetRange Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Cohesion -> Cohesion Source #
HasRange Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Cohesion -> Range Source #
LensCohesion Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods getCohesion :: Cohesion -> Cohesion Source # setCohesion :: Cohesion -> Cohesion -> Cohesion Source # mapCohesion :: (Cohesion -> Cohesion) -> Cohesion -> Cohesion Source #
EmbPrj Cohesion Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Cohesion -> S Int32 Source # icod_ :: Cohesion -> S Int32 Source # value :: Int32 -> R Cohesion Source #
type Rep Cohesion Source #
Instance details Defined in Agda.Syntax.Common type Rep Cohesion = D1 (MetaData "Cohesion" "Agda.Syntax.Common" "Agda-2.6.1-HTVbJ7KJ8pbJE1PvbUqEEQ" False) (C1 (MetaCons "Flat" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Continuous" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Squash" PrefixI False) (U1 :: Type -> Type)))

allCohesions :: [Cohesion] Source #

defaultCohesion :: Cohesion Source #

class LensCohesion a where Source #

A lens to access the Cohesion attribute in data structures. Minimal implementation: getCohesion and mapCohesion or LensModality.

Minimal complete definition

Nothing

Methods

getCohesion :: a -> Cohesion Source #

setCohesion :: Cohesion -> a -> a Source #

mapCohesion :: (Cohesion -> Cohesion) -> a -> a Source #

getCohesion :: LensModality a => a -> Cohesion Source #

mapCohesion :: LensModality a => (Cohesion -> Cohesion) -> a -> a Source #

Instances

LensCohesion ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods getCohesion :: ArgInfo -> Cohesion Source # setCohesion :: Cohesion -> ArgInfo -> ArgInfo Source # mapCohesion :: (Cohesion -> Cohesion) -> ArgInfo -> ArgInfo Source #
LensCohesion Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods getCohesion :: Cohesion -> Cohesion Source # setCohesion :: Cohesion -> Cohesion -> Cohesion Source # mapCohesion :: (Cohesion -> Cohesion) -> Cohesion -> Cohesion Source #
LensCohesion Modality Source #
Instance details Defined in Agda.Syntax.Common Methods getCohesion :: Modality -> Cohesion Source # setCohesion :: Cohesion -> Modality -> Modality Source # mapCohesion :: (Cohesion -> Cohesion) -> Modality -> Modality Source #
LensCohesion (Arg e) Source #
Instance details Defined in Agda.Syntax.Common Methods getCohesion :: Arg e -> Cohesion Source # setCohesion :: Cohesion -> Arg e -> Arg e Source # mapCohesion :: (Cohesion -> Cohesion) -> Arg e -> Arg e Source #
LensCohesion (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getCohesion :: Dom' t e -> Cohesion Source # setCohesion :: Cohesion -> Dom' t e -> Dom' t e Source # mapCohesion :: (Cohesion -> Cohesion) -> Dom' t e -> Dom' t e Source #

moreCohesion :: Cohesion -> Cohesion -> Bool Source #

Information ordering. Flat `moreCohesion` Continuous `moreCohesion` Sharp `moreCohesion` Squash

sameCohesion :: Cohesion -> Cohesion -> Bool Source #

Equality ignoring origin.

usableCohesion :: LensCohesion a => a -> Bool Source #

usableCohesion rel == False iff we cannot use a variable of rel.

composeCohesion :: Cohesion -> Cohesion -> Cohesion Source #

Cohesion composition. Squash is dominant, Continuous is neutral.

applyCohesion :: LensCohesion a => Cohesion -> a -> a Source #

Compose with cohesion flag from the left. This function is e.g. used to update the cohesion information on pattern variables a after a match against something of cohesion rel.

inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion Source #

inverseComposeCohesion r x returns the least y such that forall x, y we have x `moreCohesion` (r `composeCohesion` y) iff (r `inverseComposeCohesion` x) `moreCohesion` y (Galois connection). The above law fails for r = Squash.

inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a Source #

Left division by a Cohesion. Used e.g. to modify context when going into a rel argument.

addCohesion :: Cohesion -> Cohesion -> Cohesion Source #

Combine inferred Cohesion. The unit is Squash.

zeroCohesion :: Cohesion Source #

Cohesion forms a monoid under addition, and even a semiring.

topCohesion :: Cohesion Source #

Absorptive element under addition.

Origin of arguments (user-written, inserted or reflected)

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 # (/=) :: Origin -> Origin -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Origin # toConstr :: Origin -> Constr # dataTypeOf :: Origin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Origin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Origin) # gmapT :: (forall b. Data b => b -> b) -> Origin -> Origin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r # gmapQ :: (forall d. Data d => d -> u) -> Origin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Origin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Origin -> m Origin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin #
Ord Origin Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Origin -> Origin -> Ordering # (<) :: Origin -> Origin -> Bool # (<=) :: Origin -> Origin -> Bool # (>) :: Origin -> Origin -> Bool # (>=) :: Origin -> Origin -> Bool # max :: Origin -> Origin -> Origin # min :: Origin -> Origin -> Origin #
Show Origin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Origin -> ShowS # show :: Origin -> String # showList :: [Origin] -> ShowS #
NFData Origin Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Origin -> () #
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 # (<$) :: a -> WithOrigin b -> WithOrigin a #
Foldable WithOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods fold :: Monoid m => WithOrigin m -> m # foldMap :: Monoid m => (a -> m) -> WithOrigin a -> m # foldr :: (a -> b -> b) -> b -> WithOrigin a -> b # foldr' :: (a -> b -> b) -> b -> WithOrigin a -> b # foldl :: (b -> a -> b) -> b -> WithOrigin a -> b # foldl' :: (b -> a -> b) -> b -> WithOrigin a -> b # foldr1 :: (a -> a -> a) -> WithOrigin a -> a # foldl1 :: (a -> a -> a) -> WithOrigin a -> a # toList :: WithOrigin a -> [a] # null :: WithOrigin a -> Bool # length :: WithOrigin a -> Int # elem :: Eq a => a -> WithOrigin a -> Bool # maximum :: Ord a => WithOrigin a -> a # minimum :: Ord a => WithOrigin a -> a # sum :: Num a => WithOrigin a -> a # product :: Num a => WithOrigin a -> a #
Traversable WithOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> WithOrigin a -> f (WithOrigin b) # sequenceA :: Applicative f => WithOrigin (f a) -> f (WithOrigin a) # mapM :: Monad m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) # sequence :: Monad m => WithOrigin (m a) -> m (WithOrigin a) #
Decoration WithOrigin Source #
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 #
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] #
UniverseBi Declaration (NamedArg LHSCore) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] #
UniverseBi Declaration (NamedArg Expr) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] #
UniverseBi Declaration (NamedArg BindName) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] #
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 NamedName (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensNamed :: Lens' (Maybe NamedName) (Dom' t e) Source #
Eq a => Eq (WithOrigin a) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: WithOrigin a -> WithOrigin a -> Bool # (/=) :: WithOrigin a -> WithOrigin a -> Bool #
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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WithOrigin a) # toConstr :: WithOrigin a -> Constr # dataTypeOf :: WithOrigin a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WithOrigin a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WithOrigin a)) # gmapT :: (forall b. Data b => b -> b) -> WithOrigin a -> WithOrigin a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithOrigin a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithOrigin a -> r # gmapQ :: (forall d. Data d => d -> u) -> WithOrigin a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> WithOrigin a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithOrigin a -> m (WithOrigin a) #
Ord a => Ord (WithOrigin a) Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: WithOrigin a -> WithOrigin a -> Ordering # (<) :: WithOrigin a -> WithOrigin a -> Bool # (<=) :: WithOrigin a -> WithOrigin a -> Bool # (>) :: WithOrigin a -> WithOrigin a -> Bool # (>=) :: WithOrigin a -> WithOrigin a -> Bool # max :: WithOrigin a -> WithOrigin a -> WithOrigin a # min :: WithOrigin a -> WithOrigin a -> WithOrigin a #
Show a => Show (WithOrigin a) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> WithOrigin a -> ShowS # show :: WithOrigin a -> String # showList :: [WithOrigin a] -> ShowS #
NFData a => NFData (WithOrigin a) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: WithOrigin a -> () #
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 #
Pretty a => Pretty (WithOrigin a) Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: WithOrigin a -> Doc Source # prettyPrec :: Int -> WithOrigin a -> Doc Source # prettyList :: [WithOrigin a] -> Doc Source #
KillRange a => KillRange (WithOrigin a) Source #
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 #
IsNoName a => IsNoName (WithOrigin a) Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: WithOrigin a -> Bool 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 (WithOrigin a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: WithOrigin a -> S Int32 Source # icod_ :: WithOrigin a -> S Int32 Source # value :: Int32 -> R (WithOrigin a) Source #
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Named_ a -> m 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 #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
ToAbstract [Arg Term] [NamedArg Expr] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => [Arg Term] -> m [NamedArg Expr] Source #
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Arg r -> m (NamedArg a) Source #
AddContext ([NamedArg Name], Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #

class LensOrigin a where Source #

A lens to access the Origin attribute in data structures. Minimal implementation: getOrigin and mapOrigin or LensArgInfo.

Minimal complete definition

Nothing

Methods

getOrigin :: a -> Origin Source #

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

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

getOrigin :: LensArgInfo a => a -> Origin Source #

mapOrigin :: LensArgInfo a => (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 (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 #
LensOrigin (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getOrigin :: Dom' t e -> Origin Source # setOrigin :: Origin -> Dom' t e -> Dom' t e Source # mapOrigin :: (Origin -> Origin) -> Dom' t e -> Dom' t e 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 # (/=) :: FreeVariables -> FreeVariables -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FreeVariables # toConstr :: FreeVariables -> Constr # dataTypeOf :: FreeVariables -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FreeVariables) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FreeVariables) # gmapT :: (forall b. Data b => b -> b) -> FreeVariables -> FreeVariables # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FreeVariables -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FreeVariables -> r # gmapQ :: (forall d. Data d => d -> u) -> FreeVariables -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FreeVariables -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FreeVariables -> m FreeVariables # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FreeVariables -> m FreeVariables # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FreeVariables -> m FreeVariables #
Ord FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: FreeVariables -> FreeVariables -> Ordering # (<) :: FreeVariables -> FreeVariables -> Bool # (<=) :: FreeVariables -> FreeVariables -> Bool # (>) :: FreeVariables -> FreeVariables -> Bool # (>=) :: FreeVariables -> FreeVariables -> Bool # max :: FreeVariables -> FreeVariables -> FreeVariables # min :: FreeVariables -> FreeVariables -> FreeVariables #
Show FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> FreeVariables -> ShowS # show :: FreeVariables -> String # showList :: [FreeVariables] -> ShowS #
Semigroup FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: FreeVariables -> FreeVariables -> FreeVariables # sconcat :: NonEmpty FreeVariables -> FreeVariables # stimes :: Integral b => b -> FreeVariables -> FreeVariables #
Monoid FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: FreeVariables # mappend :: FreeVariables -> FreeVariables -> FreeVariables # mconcat :: [FreeVariables] -> FreeVariables #
NFData FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: FreeVariables -> () #
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 mapFreeVariables or LensArgInfo.

Minimal complete definition

Nothing

Methods

getFreeVariables :: a -> FreeVariables Source #

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

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

getFreeVariables :: LensArgInfo a => a -> FreeVariables Source #

mapFreeVariables :: LensArgInfo a => (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 (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 #
LensFreeVariables (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getFreeVariables :: Dom' t e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Dom' t e -> Dom' t e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom' t e -> Dom' t 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 # (/=) :: ArgInfo -> ArgInfo -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ArgInfo # toConstr :: ArgInfo -> Constr # dataTypeOf :: ArgInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ArgInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgInfo) # gmapT :: (forall b. Data b => b -> b) -> ArgInfo -> ArgInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArgInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArgInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> ArgInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ArgInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgInfo -> m ArgInfo #
Ord ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: ArgInfo -> ArgInfo -> Ordering # (<) :: ArgInfo -> ArgInfo -> Bool # (<=) :: ArgInfo -> ArgInfo -> Bool # (>) :: ArgInfo -> ArgInfo -> Bool # (>=) :: ArgInfo -> ArgInfo -> Bool # max :: ArgInfo -> ArgInfo -> ArgInfo # min :: ArgInfo -> ArgInfo -> ArgInfo #
Show ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ArgInfo -> ShowS # show :: ArgInfo -> String # showList :: [ArgInfo] -> ShowS #
NFData ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: ArgInfo -> () #
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 #
LensCohesion ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods getCohesion :: ArgInfo -> Cohesion Source # setCohesion :: Cohesion -> ArgInfo -> ArgInfo Source # mapCohesion :: (Cohesion -> Cohesion) -> 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 #
ChooseFlex ArgInfo Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: ArgInfo -> ArgInfo -> FlexChoice Source #
Unquote ArgInfo Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM ArgInfo Source #
EqualSy ArgInfo Source #	Ignore origin and free variables.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: ArgInfo -> ArgInfo -> Bool 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 Definition Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getArgInfo :: Definition -> ArgInfo Source # setArgInfo :: ArgInfo -> Definition -> Definition Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Definition -> Definition Source #
LensArgInfo (Arg a) Source #
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 #
LensArgInfo (FlexibleVar a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getArgInfo :: FlexibleVar a -> ArgInfo Source # setArgInfo :: ArgInfo -> FlexibleVar a -> FlexibleVar a Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a Source #
LensArgInfo (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getArgInfo :: Dom' t e -> ArgInfo Source # setArgInfo :: ArgInfo -> Dom' t e -> Dom' t e Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e 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 #

isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool 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 # (<$) :: a -> Arg b -> Arg a #
Foldable Arg Source #
Instance details Defined in Agda.Syntax.Common Methods fold :: Monoid m => Arg m -> m # foldMap :: Monoid m => (a -> m) -> Arg a -> m # foldr :: (a -> b -> b) -> b -> Arg a -> b # foldr' :: (a -> b -> b) -> b -> Arg a -> b # foldl :: (b -> a -> b) -> b -> Arg a -> b # foldl' :: (b -> a -> b) -> b -> Arg a -> b # foldr1 :: (a -> a -> a) -> Arg a -> a # foldl1 :: (a -> a -> a) -> Arg a -> a # toList :: Arg a -> [a] # null :: Arg a -> Bool # length :: Arg a -> Int # elem :: Eq a => a -> Arg a -> Bool # maximum :: Ord a => Arg a -> a # minimum :: Ord a => Arg a -> a # sum :: Num a => Arg a -> a # product :: Num a => Arg a -> a #
Traversable Arg Source #
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> Arg a -> f (Arg b) # sequenceA :: Applicative f => Arg (f a) -> f (Arg a) # mapM :: Monad m => (a -> m b) -> Arg a -> m (Arg b) # sequence :: Monad m => Arg (m a) -> m (Arg a) #
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 #
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM Type (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) 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] #
UniverseBi Declaration (NamedArg LHSCore) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] #
UniverseBi Declaration (NamedArg Expr) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] #
UniverseBi Declaration (NamedArg BindName) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] #
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 MOT (Exp O) Type Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type Source #
Conversion MOT (Exp O) Term Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] 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 #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: MM a (RefInfo O) -> MOT b Source #
Eq e => Eq (Arg e) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Arg e -> Arg e -> Bool # (/=) :: Arg e -> Arg e -> Bool #
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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Arg e) # toConstr :: Arg e -> Constr # dataTypeOf :: Arg e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Arg e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Arg e)) # gmapT :: (forall b. Data b => b -> b) -> Arg e -> Arg e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Arg e -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Arg e -> r # gmapQ :: (forall d. Data d => d -> u) -> Arg e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Arg e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Arg e -> m (Arg e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Arg e -> m (Arg e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Arg e -> m (Arg e) #
Ord e => Ord (Arg e) Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Arg e -> Arg e -> Ordering # (<) :: Arg e -> Arg e -> Bool # (<=) :: Arg e -> Arg e -> Bool # (>) :: Arg e -> Arg e -> Bool # (>=) :: Arg e -> Arg e -> Bool # max :: Arg e -> Arg e -> Arg e # min :: Arg e -> Arg e -> Arg e #
Show e => Show (Arg e) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Arg e -> ShowS # show :: Arg e -> String # showList :: [Arg e] -> ShowS #
NFData e => NFData (Arg e) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Arg e -> () #
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 #
LensCohesion (Arg e) Source #
Instance details Defined in Agda.Syntax.Common Methods getCohesion :: Arg e -> Cohesion Source # setCohesion :: Cohesion -> Arg e -> Arg e Source # mapCohesion :: (Cohesion -> Cohesion) -> 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 t => Free (Arg t) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Arg t -> FreeM a 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 #
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 :: MonadPretty m => Arg a -> m 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 :: (MonadFail m, ReadTCState m) => Arg a -> m 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 mentionsMetas :: HashSet 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 :: MonadDisplayForm m => Arg a -> Arg a -> MaybeT m [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 #
GetMatchables a => GetMatchables (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Arg a -> [QName] 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 #
AnyRigid a => AnyRigid (Arg a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: (MonadReduce tcm, MonadAddContext tcm) => (Nat -> tcm Bool) -> Arg a -> tcm Bool Source #
Occurs a => Occurs (Arg a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: Arg a -> OccursM (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 #
EqualSy a => EqualSy (Arg a) Source #	Ignores irrelevant arguments and modality. (And, of course, origin and free variables).
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Arg a -> Arg a -> Bool 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 #
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 #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Arg DeBruijnPattern -> Elim' NLPat 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 :: MonadReflectedToAbstract m => [Arg Term] -> m [NamedArg Expr] Source #
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Arg r -> m (NamedArg 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 :: MonadReify m => Arg i -> m (Arg a) Source # reifyWhen :: MonadReify m => Bool -> Arg i -> m (Arg a) Source #
Reify i a => Reify (Dom i) (Arg a) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Dom i -> m (Arg a) Source # reifyWhen :: MonadReify m => Bool -> Dom i -> m (Arg a) Source #
NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m) => Arg p -> m (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 #
PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b) 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 #
AddContext ([NamedArg Name], Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
AddContext ([Arg Name], Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m 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 Args, 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 #

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] #
UniverseBi Declaration (NamedArg LHSCore) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] #
UniverseBi Declaration (NamedArg Expr) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] #
UniverseBi Declaration (NamedArg BindName) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] #
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 # (<$) :: a -> Named name b -> Named name a #
Foldable (Named name) Source #
Instance details Defined in Agda.Syntax.Common Methods fold :: Monoid m => Named name m -> m # foldMap :: Monoid m => (a -> m) -> Named name a -> m # foldr :: (a -> b -> b) -> b -> Named name a -> b # foldr' :: (a -> b -> b) -> b -> Named name a -> b # foldl :: (b -> a -> b) -> b -> Named name a -> b # foldl' :: (b -> a -> b) -> b -> Named name a -> b # foldr1 :: (a -> a -> a) -> Named name a -> a # foldl1 :: (a -> a -> a) -> Named name a -> a # toList :: Named name a -> [a] # null :: Named name a -> Bool # length :: Named name a -> Int # elem :: Eq a => a -> Named name a -> Bool # maximum :: Ord a => Named name a -> a # minimum :: Ord a => Named name a -> a # sum :: Num a => Named name a -> a # product :: Num a => Named name a -> a #
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) # sequenceA :: Applicative f => Named name (f a) -> f (Named name a) # mapM :: Monad m => (a -> m b) -> Named name a -> m (Named name b) # sequence :: Monad m => Named name (m a) -> m (Named name a) #
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 :: MonadPretty m => Named_ a -> m 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 #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
ToAbstract [Arg Term] [NamedArg Expr] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => [Arg Term] -> m [NamedArg Expr] Source #
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Arg r -> m (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 # (/=) :: Named name a -> Named name a -> Bool #
(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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Named name a) # toConstr :: Named name a -> Constr # dataTypeOf :: Named name a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Named name a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Named name a)) # gmapT :: (forall b. Data b => b -> b) -> Named name a -> Named name a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r # gmapQ :: (forall d. Data d => d -> u) -> Named name a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Named name a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) #
(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 # (<) :: Named name a -> Named name a -> Bool # (<=) :: Named name a -> Named name a -> Bool # (>) :: Named name a -> Named name a -> Bool # (>=) :: Named name a -> Named name a -> Bool # max :: Named name a -> Named name a -> Named name a # min :: Named name a -> Named name a -> Named name a #
(Show name, Show a) => Show (Named name a) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Named name a -> ShowS # show :: Named name a -> String # showList :: [Named name a] -> ShowS #
(NFData name, NFData a) => NFData (Named name a) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Named name a -> () #
(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 #
AddContext ([NamedArg Name], Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # contextSize :: ([NamedArg Name], Type) -> Nat 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 #
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 #
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 #
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 :: MonadReflectedToAbstract m => Named name r -> m (Named name a) Source #
Reify i a => Reify (Named n i) (Named n a) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => Named n i -> m (Named n a) Source # reifyWhen :: MonadReify m => Bool -> Named n i -> m (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 NamedName Source #

Standard naming.

type NamedName = WithOrigin (Ranged ArgName) Source #

Standard argument names.

sameName :: NamedName -> NamedName -> Bool Source #

Equality of argument names of things modulo Range' and Origin.

unnamed :: a -> Named name a Source #

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

userNamed :: Ranged ArgName -> a -> Named_ a Source #

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

Accessor/editor for the nameOf component.

Minimal complete definition

Nothing

Methods

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

lensNamed :: (Decoration f, LensNamed name b, f b ~ a) => Lens' (Maybe name) a Source #

Instances

LensNamed name (Maybe name) Source #
Instance details Defined in Agda.Syntax.Common Methods lensNamed :: Lens' (Maybe name) (Maybe name) Source #
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 #
LensNamed NamedName (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensNamed :: Lens' (Maybe NamedName) (Dom' t e) 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 #

bareNameOf :: LensNamed NamedName a => a -> Maybe ArgName Source #

bareNameWithDefault :: LensNamed NamedName a => ArgName -> a -> ArgName Source #

namedSame :: (LensNamed NamedName a, LensNamed NamedName b) => a -> b -> Bool Source #

Equality of argument names of things modulo Range' and Origin.

fittingNamedArg :: (LensNamed NamedName arg, LensHiding arg, LensNamed NamedName dom, LensHiding dom) => arg -> dom -> Maybe Bool Source #

Does an argument arg fit the shape dom of the next expected argument?

The hiding has to match, and if the argument has a name, it should match the name of the domain.

Nothing should be __IMPOSSIBLE__, so use as @fromMaybe IMPOSSIBLE $ fittingNamedArg arg dom@

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.

updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b) Source #

setNamedArg :: NamedArg a -> b -> NamedArg b Source #

setNamedArg a b = updateNamedArg (const b) a

ArgName

type ArgName = String Source #

Names in binders and arguments.

argNameToString :: ArgName -> String Source #

stringToArgName :: String -> ArgName Source #

appendArgNames :: ArgName -> ArgName -> ArgName Source #

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 # (<$) :: a -> Ranged b -> Ranged a #
Foldable Ranged Source #
Instance details Defined in Agda.Syntax.Common Methods fold :: Monoid m => Ranged m -> m # foldMap :: Monoid m => (a -> m) -> Ranged a -> m # foldr :: (a -> b -> b) -> b -> Ranged a -> b # foldr' :: (a -> b -> b) -> b -> Ranged a -> b # foldl :: (b -> a -> b) -> b -> Ranged a -> b # foldl' :: (b -> a -> b) -> b -> Ranged a -> b # foldr1 :: (a -> a -> a) -> Ranged a -> a # foldl1 :: (a -> a -> a) -> Ranged a -> a # toList :: Ranged a -> [a] # null :: Ranged a -> Bool # length :: Ranged a -> Int # elem :: Eq a => a -> Ranged a -> Bool # maximum :: Ord a => Ranged a -> a # minimum :: Ord a => Ranged a -> a # sum :: Num a => Ranged a -> a # product :: Num a => Ranged a -> a #
Traversable Ranged Source #
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> Ranged a -> f (Ranged b) # sequenceA :: Applicative f => Ranged (f a) -> f (Ranged a) # mapM :: Monad m => (a -> m b) -> Ranged a -> m (Ranged b) # sequence :: Monad m => Ranged (m a) -> m (Ranged a) #
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] #
UniverseBi Declaration (NamedArg LHSCore) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg LHSCore] #
UniverseBi Declaration (NamedArg Expr) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg Expr] #
UniverseBi Declaration (NamedArg BindName) Source #
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [NamedArg BindName] #
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 NamedName (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensNamed :: Lens' (Maybe NamedName) (Dom' t e) Source #
Eq a => Eq (Ranged a) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Ranged a -> Ranged a -> Bool # (/=) :: Ranged a -> Ranged a -> Bool #
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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ranged a) # toConstr :: Ranged a -> Constr # dataTypeOf :: Ranged a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Ranged a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ranged a)) # gmapT :: (forall b. Data b => b -> b) -> Ranged a -> Ranged a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r # gmapQ :: (forall d. Data d => d -> u) -> Ranged a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Ranged a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) #
Ord a => Ord (Ranged a) Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Ranged a -> Ranged a -> Ordering # (<) :: Ranged a -> Ranged a -> Bool # (<=) :: Ranged a -> Ranged a -> Bool # (>) :: Ranged a -> Ranged a -> Bool # (>=) :: Ranged a -> Ranged a -> Bool # max :: Ranged a -> Ranged a -> Ranged a # min :: Ranged a -> Ranged a -> Ranged a #
Show a => Show (Ranged a) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Ranged a -> ShowS # show :: Ranged a -> String # showList :: [Ranged a] -> ShowS #
NFData a => NFData (Ranged a) Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Common Methods rnf :: Ranged a -> () #
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 #
IsNoName a => IsNoName (Ranged a) Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: Ranged a -> Bool 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 :: MonadPretty m => Named_ a -> m 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 #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
ToAbstract [Arg Term] [NamedArg Expr] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => [Arg Term] -> m [NamedArg Expr] Source #
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => Arg r -> m (NamedArg a) Source #
AddContext ([NamedArg Name], Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m 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 # maxBound :: ConOrigin #
Enum ConOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: ConOrigin -> ConOrigin # pred :: ConOrigin -> ConOrigin # toEnum :: Int -> ConOrigin # fromEnum :: ConOrigin -> Int # enumFrom :: ConOrigin -> [ConOrigin] # enumFromThen :: ConOrigin -> ConOrigin -> [ConOrigin] # enumFromTo :: ConOrigin -> ConOrigin -> [ConOrigin] # enumFromThenTo :: ConOrigin -> ConOrigin -> ConOrigin -> [ConOrigin] #
Eq ConOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: ConOrigin -> ConOrigin -> Bool # (/=) :: ConOrigin -> ConOrigin -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConOrigin # toConstr :: ConOrigin -> Constr # dataTypeOf :: ConOrigin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConOrigin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConOrigin) # gmapT :: (forall b. Data b => b -> b) -> ConOrigin -> ConOrigin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r # gmapQ :: (forall d. Data d => d -> u) -> ConOrigin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ConOrigin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin #
Ord ConOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: ConOrigin -> ConOrigin -> Ordering # (<) :: ConOrigin -> ConOrigin -> Bool # (<=) :: ConOrigin -> ConOrigin -> Bool # (>) :: ConOrigin -> ConOrigin -> Bool # (>=) :: ConOrigin -> ConOrigin -> Bool # max :: ConOrigin -> ConOrigin -> ConOrigin # min :: ConOrigin -> ConOrigin -> ConOrigin #
Show ConOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ConOrigin -> ShowS # show :: ConOrigin -> String # showList :: [ConOrigin] -> ShowS #
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 # maxBound :: ProjOrigin #
Enum ProjOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: ProjOrigin -> ProjOrigin # pred :: ProjOrigin -> ProjOrigin # toEnum :: Int -> ProjOrigin # fromEnum :: ProjOrigin -> Int # enumFrom :: ProjOrigin -> [ProjOrigin] # enumFromThen :: ProjOrigin -> ProjOrigin -> [ProjOrigin] # enumFromTo :: ProjOrigin -> ProjOrigin -> [ProjOrigin] # enumFromThenTo :: ProjOrigin -> ProjOrigin -> ProjOrigin -> [ProjOrigin] #
Eq ProjOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: ProjOrigin -> ProjOrigin -> Bool # (/=) :: ProjOrigin -> ProjOrigin -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProjOrigin # toConstr :: ProjOrigin -> Constr # dataTypeOf :: ProjOrigin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProjOrigin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProjOrigin) # gmapT :: (forall b. Data b => b -> b) -> ProjOrigin -> ProjOrigin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProjOrigin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProjOrigin -> r # gmapQ :: (forall d. Data d => d -> u) -> ProjOrigin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ProjOrigin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjOrigin -> m ProjOrigin #
Ord ProjOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: ProjOrigin -> ProjOrigin -> Ordering # (<) :: ProjOrigin -> ProjOrigin -> Bool # (<=) :: ProjOrigin -> ProjOrigin -> Bool # (>) :: ProjOrigin -> ProjOrigin -> Bool # (>=) :: ProjOrigin -> ProjOrigin -> Bool # max :: ProjOrigin -> ProjOrigin -> ProjOrigin # min :: ProjOrigin -> ProjOrigin -> ProjOrigin #
Show ProjOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ProjOrigin -> ShowS # show :: ProjOrigin -> String # showList :: [ProjOrigin] -> ShowS #
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 # (/=) :: DataOrRecord -> DataOrRecord -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataOrRecord # toConstr :: DataOrRecord -> Constr # dataTypeOf :: DataOrRecord -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataOrRecord) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataOrRecord) # gmapT :: (forall b. Data b => b -> b) -> DataOrRecord -> DataOrRecord # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r # gmapQ :: (forall d. Data d => d -> u) -> DataOrRecord -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DataOrRecord -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord #
Ord DataOrRecord Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: DataOrRecord -> DataOrRecord -> Ordering # (<) :: DataOrRecord -> DataOrRecord -> Bool # (<=) :: DataOrRecord -> DataOrRecord -> Bool # (>) :: DataOrRecord -> DataOrRecord -> Bool # (>=) :: DataOrRecord -> DataOrRecord -> Bool # max :: DataOrRecord -> DataOrRecord -> DataOrRecord # min :: DataOrRecord -> DataOrRecord -> DataOrRecord #
Show DataOrRecord Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> DataOrRecord -> ShowS # show :: DataOrRecord -> String # showList :: [DataOrRecord] -> ShowS #
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 # (/=) :: IsInfix -> IsInfix -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInfix # toConstr :: IsInfix -> Constr # dataTypeOf :: IsInfix -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInfix) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInfix) # gmapT :: (forall b. Data b => b -> b) -> IsInfix -> IsInfix # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r # gmapQ :: (forall d. Data d => d -> u) -> IsInfix -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInfix -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix #
Ord IsInfix Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: IsInfix -> IsInfix -> Ordering # (<) :: IsInfix -> IsInfix -> Bool # (<=) :: IsInfix -> IsInfix -> Bool # (>) :: IsInfix -> IsInfix -> Bool # (>=) :: IsInfix -> IsInfix -> Bool # max :: IsInfix -> IsInfix -> IsInfix # min :: IsInfix -> IsInfix -> IsInfix #
Show IsInfix Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsInfix -> ShowS # show :: IsInfix -> String # showList :: [IsInfix] -> ShowS #

private blocks, public imports

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

Instances

Eq Access Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Access -> Access -> Bool # (/=) :: Access -> Access -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Access # toConstr :: Access -> Constr # dataTypeOf :: Access -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Access) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Access) # gmapT :: (forall b. Data b => b -> b) -> Access -> Access # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r # gmapQ :: (forall d. Data d => d -> u) -> Access -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Access -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Access -> m Access # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access #
Ord Access Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Access -> Access -> Ordering # (<) :: Access -> Access -> Bool # (<=) :: Access -> Access -> Bool # (>) :: Access -> Access -> Bool # (>=) :: Access -> Access -> Bool # max :: Access -> Access -> Access # min :: Access -> Access -> Access #
Show Access Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Access -> ShowS # show :: Access -> String # showList :: [Access] -> ShowS #
NFData Access Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Access -> () #
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 #

abstract blocks

data IsAbstract Source #

Abstract or concrete.

Constructors

AbstractDef
ConcreteDef

Instances

Eq IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsAbstract -> IsAbstract -> Bool # (/=) :: IsAbstract -> IsAbstract -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsAbstract # toConstr :: IsAbstract -> Constr # dataTypeOf :: IsAbstract -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsAbstract) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsAbstract) # gmapT :: (forall b. Data b => b -> b) -> IsAbstract -> IsAbstract # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsAbstract -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsAbstract -> r # gmapQ :: (forall d. Data d => d -> u) -> IsAbstract -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsAbstract -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsAbstract -> m IsAbstract #
Ord IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: IsAbstract -> IsAbstract -> Ordering # (<) :: IsAbstract -> IsAbstract -> Bool # (<=) :: IsAbstract -> IsAbstract -> Bool # (>) :: IsAbstract -> IsAbstract -> Bool # (>=) :: IsAbstract -> IsAbstract -> Bool # max :: IsAbstract -> IsAbstract -> IsAbstract # min :: IsAbstract -> IsAbstract -> IsAbstract #
Show IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsAbstract -> ShowS # show :: IsAbstract -> String # showList :: [IsAbstract] -> ShowS #
Semigroup IsAbstract Source #	Semigroup computes if any of several is an `AbstractDef`.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: IsAbstract -> IsAbstract -> IsAbstract # sconcat :: NonEmpty IsAbstract -> IsAbstract # stimes :: Integral b => b -> IsAbstract -> IsAbstract #
Monoid IsAbstract Source #	Default is `ConcreteDef`.
Instance details Defined in Agda.Syntax.Common Methods mempty :: IsAbstract # mappend :: IsAbstract -> IsAbstract -> IsAbstract # mconcat :: [IsAbstract] -> IsAbstract #
KillRange IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsAbstract Source #
AnyIsAbstract IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods anyIsAbstract :: IsAbstract -> IsAbstract Source #
LensIsAbstract IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods lensIsAbstract :: Lens' IsAbstract 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 #

class LensIsAbstract a where Source #

Methods

lensIsAbstract :: Lens' IsAbstract a Source #

Instances

LensIsAbstract IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods lensIsAbstract :: Lens' IsAbstract IsAbstract Source #
LensIsAbstract TCEnv Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensIsAbstract :: Lens' IsAbstract TCEnv Source #
LensIsAbstract MetaInfo Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensIsAbstract :: Lens' IsAbstract MetaInfo Source #
LensIsAbstract (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods lensIsAbstract :: Lens' IsAbstract (DefInfo' t) Source #
LensIsAbstract (Closure a) Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lensIsAbstract :: Lens' IsAbstract (Closure a) Source #

class AnyIsAbstract a where Source #

Is any element of a collection an AbstractDef.

Minimal complete definition

Nothing

Methods

anyIsAbstract :: a -> IsAbstract Source #

anyIsAbstract :: (Foldable t, AnyIsAbstract b, t b ~ a) => a -> IsAbstract Source #

Instances

AnyIsAbstract IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods anyIsAbstract :: IsAbstract -> IsAbstract Source #
AnyIsAbstract a => AnyIsAbstract [a] Source #
Instance details Defined in Agda.Syntax.Common Methods anyIsAbstract :: [a] -> IsAbstract Source #
AnyIsAbstract a => AnyIsAbstract (Maybe a) Source #
Instance details Defined in Agda.Syntax.Common Methods anyIsAbstract :: Maybe a -> IsAbstract Source #
AnyIsAbstract (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods anyIsAbstract :: DefInfo' t -> IsAbstract Source #

instance blocks

data IsInstance Source #

Is this definition eligible for instance search?

Constructors

InstanceDef Range	Range of the `instance` keyword.
NotInstanceDef

Instances

Eq IsInstance Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsInstance -> IsInstance -> Bool # (/=) :: IsInstance -> IsInstance -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInstance # toConstr :: IsInstance -> Constr # dataTypeOf :: IsInstance -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInstance) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInstance) # gmapT :: (forall b. Data b => b -> b) -> IsInstance -> IsInstance # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInstance -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInstance -> r # gmapQ :: (forall d. Data d => d -> u) -> IsInstance -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInstance -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInstance -> m IsInstance #
Ord IsInstance Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: IsInstance -> IsInstance -> Ordering # (<) :: IsInstance -> IsInstance -> Bool # (<=) :: IsInstance -> IsInstance -> Bool # (>) :: IsInstance -> IsInstance -> Bool # (>=) :: IsInstance -> IsInstance -> Bool # max :: IsInstance -> IsInstance -> IsInstance # min :: IsInstance -> IsInstance -> IsInstance #
Show IsInstance Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsInstance -> ShowS # show :: IsInstance -> String # showList :: [IsInstance] -> ShowS #
NFData IsInstance Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: IsInstance -> () #
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 #

macro blocks

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 # (/=) :: IsMacro -> IsMacro -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsMacro # toConstr :: IsMacro -> Constr # dataTypeOf :: IsMacro -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsMacro) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsMacro) # gmapT :: (forall b. Data b => b -> b) -> IsMacro -> IsMacro # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r # gmapQ :: (forall d. Data d => d -> u) -> IsMacro -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsMacro -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro #
Ord IsMacro Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: IsMacro -> IsMacro -> Ordering # (<) :: IsMacro -> IsMacro -> Bool # (<=) :: IsMacro -> IsMacro -> Bool # (>) :: IsMacro -> IsMacro -> Bool # (>=) :: IsMacro -> IsMacro -> Bool # max :: IsMacro -> IsMacro -> IsMacro # min :: IsMacro -> IsMacro -> IsMacro #
Show IsMacro Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsMacro -> ShowS # show :: IsMacro -> String # showList :: [IsMacro] -> ShowS #
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 #

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 # pred :: NameId -> NameId # toEnum :: Int -> NameId # fromEnum :: NameId -> Int # enumFrom :: NameId -> [NameId] # enumFromThen :: NameId -> NameId -> [NameId] # enumFromTo :: NameId -> NameId -> [NameId] # enumFromThenTo :: NameId -> NameId -> NameId -> [NameId] #
Eq NameId Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: NameId -> NameId -> Bool # (/=) :: NameId -> NameId -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameId # toConstr :: NameId -> Constr # dataTypeOf :: NameId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameId) # gmapT :: (forall b. Data b => b -> b) -> NameId -> NameId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r # gmapQ :: (forall d. Data d => d -> u) -> NameId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NameId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameId -> m NameId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId #
Ord NameId Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: NameId -> NameId -> Ordering # (<) :: NameId -> NameId -> Bool # (<=) :: NameId -> NameId -> Bool # (>) :: NameId -> NameId -> Bool # (>=) :: NameId -> NameId -> Bool # max :: NameId -> NameId -> NameId # min :: NameId -> NameId -> NameId #
Show NameId Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> NameId -> ShowS # show :: NameId -> String # showList :: [NameId] -> ShowS #
Generic NameId Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep NameId :: Type -> Type # Methods from :: NameId -> Rep NameId x # to :: Rep NameId x -> NameId #
Hashable NameId Source #
Instance details Defined in Agda.Syntax.Common Methods hashWithSalt :: Int -> NameId -> Int # hash :: NameId -> Int #
NFData NameId Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: NameId -> () #
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 #
Monad m => MonadFresh NameId (PureConversionT m) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m 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.1-HTVbJ7KJ8pbJE1PvbUqEEQ" 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 # pred :: MetaId -> MetaId # toEnum :: Int -> MetaId # fromEnum :: MetaId -> Int # enumFrom :: MetaId -> [MetaId] # enumFromThen :: MetaId -> MetaId -> [MetaId] # enumFromTo :: MetaId -> MetaId -> [MetaId] # enumFromThenTo :: MetaId -> MetaId -> MetaId -> [MetaId] #
Eq MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: MetaId -> MetaId -> Bool # (/=) :: MetaId -> MetaId -> Bool #
Integral MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods quot :: MetaId -> MetaId -> MetaId # rem :: MetaId -> MetaId -> MetaId # div :: MetaId -> MetaId -> MetaId # mod :: MetaId -> MetaId -> MetaId # quotRem :: MetaId -> MetaId -> (MetaId, MetaId) # divMod :: MetaId -> MetaId -> (MetaId, MetaId) # toInteger :: MetaId -> Integer #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaId # toConstr :: MetaId -> Constr # dataTypeOf :: MetaId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaId) # gmapT :: (forall b. Data b => b -> b) -> MetaId -> MetaId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r # gmapQ :: (forall d. Data d => d -> u) -> MetaId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId #
Num MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods (+) :: MetaId -> MetaId -> MetaId # (-) :: MetaId -> MetaId -> MetaId # (*) :: MetaId -> MetaId -> MetaId # negate :: MetaId -> MetaId # abs :: MetaId -> MetaId # signum :: MetaId -> MetaId # fromInteger :: Integer -> MetaId #
Ord MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: MetaId -> MetaId -> Ordering # (<) :: MetaId -> MetaId -> Bool # (<=) :: MetaId -> MetaId -> Bool # (>) :: MetaId -> MetaId -> Bool # (>=) :: MetaId -> MetaId -> Bool # max :: MetaId -> MetaId -> MetaId # min :: MetaId -> MetaId -> MetaId #
Real MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods toRational :: MetaId -> Rational #
Show MetaId Source #	Show non-record version of this newtype.
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> MetaId -> ShowS # show :: MetaId -> String # showList :: [MetaId] -> ShowS #
Generic MetaId Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep MetaId :: Type -> Type # Methods from :: MetaId -> Rep MetaId x # to :: Rep MetaId x -> MetaId #
Hashable MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods hashWithSalt :: Int -> MetaId -> Int # hash :: MetaId -> Int #
NFData MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: MetaId -> () #
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 :: MonadPretty m => MetaId -> m Doc Source #
UnFreezeMeta MetaId Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #
IsInstantiatedMeta MetaId Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m 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 #
Singleton MetaId () Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: MetaId -> () Source #
Singleton MetaId MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: MetaId -> MetaSet Source #
Reify MetaId Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => MetaId -> m Expr Source # reifyWhen :: MonadReify m => Bool -> MetaId -> m Expr Source #
type Rep MetaId Source #
Instance details Defined in Agda.Syntax.Common type Rep MetaId = D1 (MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.1-HTVbJ7KJ8pbJE1PvbUqEEQ" True) (C1 (MetaCons "MetaId" PrefixI True) (S1 (MetaSel (Just "metaId") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Nat)))

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 # (/=) :: PositionInName -> PositionInName -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PositionInName # toConstr :: PositionInName -> Constr # dataTypeOf :: PositionInName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PositionInName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PositionInName) # gmapT :: (forall b. Data b => b -> b) -> PositionInName -> PositionInName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PositionInName -> r # gmapQ :: (forall d. Data d => d -> u) -> PositionInName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PositionInName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PositionInName -> m PositionInName #
Ord PositionInName Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: PositionInName -> PositionInName -> Ordering # (<) :: PositionInName -> PositionInName -> Bool # (<=) :: PositionInName -> PositionInName -> Bool # (>) :: PositionInName -> PositionInName -> Bool # (>=) :: PositionInName -> PositionInName -> Bool # max :: PositionInName -> PositionInName -> PositionInName # min :: PositionInName -> PositionInName -> PositionInName #
Show PositionInName Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> PositionInName -> ShowS # show :: PositionInName -> String # showList :: [PositionInName] -> ShowS #

data MaybePlaceholder e Source #

Placeholders are used to represent the underscores in a section.

Constructors

Placeholder !PositionInName
NoPlaceholder !(Maybe PositionInName) e	The second argument is used only (but not always) for name parts other than underscores.

Instances

Functor MaybePlaceholder Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b # (<$) :: a -> MaybePlaceholder b -> MaybePlaceholder a #
Foldable MaybePlaceholder Source #
Instance details Defined in Agda.Syntax.Common Methods fold :: Monoid m => MaybePlaceholder m -> m # foldMap :: Monoid m => (a -> m) -> MaybePlaceholder a -> m # foldr :: (a -> b -> b) -> b -> MaybePlaceholder a -> b # foldr' :: (a -> b -> b) -> b -> MaybePlaceholder a -> b # foldl :: (b -> a -> b) -> b -> MaybePlaceholder a -> b # foldl' :: (b -> a -> b) -> b -> MaybePlaceholder a -> b # foldr1 :: (a -> a -> a) -> MaybePlaceholder a -> a # foldl1 :: (a -> a -> a) -> MaybePlaceholder a -> a # toList :: MaybePlaceholder a -> [a] # null :: MaybePlaceholder a -> Bool # length :: MaybePlaceholder a -> Int # elem :: Eq a => a -> MaybePlaceholder a -> Bool # maximum :: Ord a => MaybePlaceholder a -> a # minimum :: Ord a => MaybePlaceholder a -> a # sum :: Num a => MaybePlaceholder a -> a # product :: Num a => MaybePlaceholder a -> a #
Traversable MaybePlaceholder Source #
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> MaybePlaceholder a -> f (MaybePlaceholder b) # sequenceA :: Applicative f => MaybePlaceholder (f a) -> f (MaybePlaceholder a) # mapM :: Monad m => (a -> m b) -> MaybePlaceholder a -> m (MaybePlaceholder b) # sequence :: Monad m => MaybePlaceholder (m a) -> m (MaybePlaceholder a) #
Eq e => Eq (MaybePlaceholder e) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (/=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool #
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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MaybePlaceholder e) # toConstr :: MaybePlaceholder e -> Constr # dataTypeOf :: MaybePlaceholder e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (MaybePlaceholder e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (MaybePlaceholder e)) # gmapT :: (forall b. Data b => b -> b) -> MaybePlaceholder e -> MaybePlaceholder e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MaybePlaceholder e -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MaybePlaceholder e -> r # gmapQ :: (forall d. Data d => d -> u) -> MaybePlaceholder e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MaybePlaceholder e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MaybePlaceholder e -> m (MaybePlaceholder e) #
Ord e => Ord (MaybePlaceholder e) Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: MaybePlaceholder e -> MaybePlaceholder e -> Ordering # (<) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (<=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (>) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (>=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # max :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e # min :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e #
Show e => Show (MaybePlaceholder e) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> MaybePlaceholder e -> ShowS # show :: MaybePlaceholder e -> String # showList :: [MaybePlaceholder e] -> ShowS #
NFData a => NFData (MaybePlaceholder a) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: MaybePlaceholder a -> () #
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 # pred :: InteractionId -> InteractionId # toEnum :: Int -> InteractionId # fromEnum :: InteractionId -> Int # enumFrom :: InteractionId -> [InteractionId] # enumFromThen :: InteractionId -> InteractionId -> [InteractionId] # enumFromTo :: InteractionId -> InteractionId -> [InteractionId] # enumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId] #
Eq InteractionId Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: InteractionId -> InteractionId -> Bool # (/=) :: InteractionId -> InteractionId -> Bool #
Integral InteractionId Source #
Instance details Defined in Agda.Syntax.Common Methods quot :: InteractionId -> InteractionId -> InteractionId # rem :: InteractionId -> InteractionId -> InteractionId # div :: InteractionId -> InteractionId -> InteractionId # mod :: InteractionId -> InteractionId -> InteractionId # quotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId) # divMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId) # toInteger :: InteractionId -> Integer #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InteractionId # toConstr :: InteractionId -> Constr # dataTypeOf :: InteractionId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InteractionId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InteractionId) # gmapT :: (forall b. Data b => b -> b) -> InteractionId -> InteractionId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InteractionId -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InteractionId -> r # gmapQ :: (forall d. Data d => d -> u) -> InteractionId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> InteractionId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InteractionId -> m InteractionId #
Num InteractionId Source #
Instance details Defined in Agda.Syntax.Common Methods (+) :: InteractionId -> InteractionId -> InteractionId # (-) :: InteractionId -> InteractionId -> InteractionId # (*) :: InteractionId -> InteractionId -> InteractionId # negate :: InteractionId -> InteractionId # abs :: InteractionId -> InteractionId # signum :: InteractionId -> InteractionId # fromInteger :: Integer -> InteractionId #
Ord InteractionId Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: InteractionId -> InteractionId -> Ordering # (<) :: InteractionId -> InteractionId -> Bool # (<=) :: InteractionId -> InteractionId -> Bool # (>) :: InteractionId -> InteractionId -> Bool # (>=) :: InteractionId -> InteractionId -> Bool # max :: InteractionId -> InteractionId -> InteractionId # min :: InteractionId -> InteractionId -> InteractionId #
Read InteractionId Source #
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS InteractionId # readList :: ReadS [InteractionId] # readPrec :: ReadPrec InteractionId # readListPrec :: ReadPrec [InteractionId] #
Real InteractionId Source #
Instance details Defined in Agda.Syntax.Common Methods toRational :: InteractionId -> Rational #
Show InteractionId Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> InteractionId -> ShowS # show :: InteractionId -> String # showList :: [InteractionId] -> ShowS #
ToJSON InteractionId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: InteractionId -> Value # toEncoding :: InteractionId -> Encoding # toJSONList :: [InteractionId] -> Value # toEncodingList :: [InteractionId] -> Encoding #
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 #
EncodeTCM InteractionId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: InteractionId -> TCM Value 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 #

Fixity

type PrecedenceLevel = Double Source #

Precedence levels for operators.

data FixityLevel Source #

Constructors

Unrelated	No fixity declared.
Related !PrecedenceLevel	Fixity level declared as the number.

Instances

Eq FixityLevel Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: FixityLevel -> FixityLevel -> Bool # (/=) :: FixityLevel -> FixityLevel -> Bool #
Data FixityLevel 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) -> FixityLevel -> c FixityLevel # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FixityLevel # toConstr :: FixityLevel -> Constr # dataTypeOf :: FixityLevel -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FixityLevel) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FixityLevel) # gmapT :: (forall b. Data b => b -> b) -> FixityLevel -> FixityLevel # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FixityLevel -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FixityLevel -> r # gmapQ :: (forall d. Data d => d -> u) -> FixityLevel -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FixityLevel -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FixityLevel -> m FixityLevel #
Ord FixityLevel Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: FixityLevel -> FixityLevel -> Ordering # (<) :: FixityLevel -> FixityLevel -> Bool # (<=) :: FixityLevel -> FixityLevel -> Bool # (>) :: FixityLevel -> FixityLevel -> Bool # (>=) :: FixityLevel -> FixityLevel -> Bool # max :: FixityLevel -> FixityLevel -> FixityLevel # min :: FixityLevel -> FixityLevel -> FixityLevel #
Show FixityLevel Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> FixityLevel -> ShowS # show :: FixityLevel -> String # showList :: [FixityLevel] -> ShowS #
Null FixityLevel Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: FixityLevel Source # null :: FixityLevel -> Bool Source #
EmbPrj FixityLevel Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FixityLevel -> S Int32 Source # icod_ :: FixityLevel -> S Int32 Source # value :: Int32 -> R FixityLevel Source #
ToTerm FixityLevel Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (FixityLevel -> Term) Source # toTermR :: TCM (FixityLevel -> ReduceM Term) Source #

data Associativity Source #

Associativity.

Constructors

NonAssoc
LeftAssoc
RightAssoc

Instances

Eq Associativity Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Associativity -> Associativity -> Bool # (/=) :: Associativity -> Associativity -> Bool #
Data Associativity 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) -> Associativity -> c Associativity # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Associativity # toConstr :: Associativity -> Constr # dataTypeOf :: Associativity -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Associativity) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Associativity) # gmapT :: (forall b. Data b => b -> b) -> Associativity -> Associativity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Associativity -> r # gmapQ :: (forall d. Data d => d -> u) -> Associativity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Associativity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Associativity -> m Associativity #
Ord Associativity Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Associativity -> Associativity -> Ordering # (<) :: Associativity -> Associativity -> Bool # (<=) :: Associativity -> Associativity -> Bool # (>) :: Associativity -> Associativity -> Bool # (>=) :: Associativity -> Associativity -> Bool # max :: Associativity -> Associativity -> Associativity # min :: Associativity -> Associativity -> Associativity #
Show Associativity Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Associativity -> ShowS # show :: Associativity -> String # showList :: [Associativity] -> ShowS #
EmbPrj Associativity Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Associativity -> S Int32 Source # icod_ :: Associativity -> S Int32 Source # value :: Int32 -> R Associativity Source #
ToTerm Associativity Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Associativity -> Term) Source # toTermR :: TCM (Associativity -> ReduceM Term) Source #

data Fixity Source #

Fixity of operators.

Constructors

Fixity
Fields fixityRange :: Range Range of the whole fixity declaration. fixityLevel :: !FixityLevel fixityAssoc :: !Associativity

Instances

Eq Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Fixity -> Fixity -> Bool # (/=) :: Fixity -> Fixity -> Bool #
Data Fixity 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) -> Fixity -> c Fixity # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity # toConstr :: Fixity -> Constr # dataTypeOf :: Fixity -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity) # gmapT :: (forall b. Data b => b -> b) -> Fixity -> Fixity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity -> r # gmapQ :: (forall d. Data d => d -> u) -> Fixity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity -> m Fixity #
Ord Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Fixity -> Fixity -> Ordering # (<) :: Fixity -> Fixity -> Bool # (<=) :: Fixity -> Fixity -> Bool # (>) :: Fixity -> Fixity -> Bool # (>=) :: Fixity -> Fixity -> Bool # max :: Fixity -> Fixity -> Fixity # min :: Fixity -> Fixity -> Fixity #
Show Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Fixity -> ShowS # show :: Fixity -> String # showList :: [Fixity] -> ShowS #
NFData Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Fixity -> () #
Null Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Fixity Source # null :: Fixity -> Bool Source #
Pretty Fixity Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Fixity -> Doc Source # prettyPrec :: Int -> Fixity -> Doc Source # prettyList :: [Fixity] -> Doc Source #
KillRange Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Fixity Source #
HasRange Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Fixity -> Range Source #
LensFixity Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods lensFixity :: Lens' Fixity Fixity Source #
EmbPrj Fixity Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity -> S Int32 Source # icod_ :: Fixity -> S Int32 Source # value :: Int32 -> R Fixity Source #
ToTerm Fixity Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity -> Term) Source # toTermR :: TCM (Fixity -> ReduceM Term) Source #

noFixity :: Fixity Source #

defaultFixity :: Fixity Source #

Notation coupled with `Fixity`

data Fixity' Source #

The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.

Constructors

Fixity'
Fields theFixity :: !Fixity theNotation :: Notation theNameRange :: Range Range of the name in the fixity declaration (used for correct highlighting, see issue #2140).

Instances

Eq Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Fixity' -> Fixity' -> Bool # (/=) :: Fixity' -> Fixity' -> Bool #
Data Fixity' 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) -> Fixity' -> c Fixity' # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Fixity' # toConstr :: Fixity' -> Constr # dataTypeOf :: Fixity' -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Fixity') # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Fixity') # gmapT :: (forall b. Data b => b -> b) -> Fixity' -> Fixity' # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fixity' -> r # gmapQ :: (forall d. Data d => d -> u) -> Fixity' -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Fixity' -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fixity' -> m Fixity' #
Show Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Fixity' -> ShowS # show :: Fixity' -> String # showList :: [Fixity'] -> ShowS #
NFData Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Fixity' -> () #
Null Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Fixity' Source # null :: Fixity' -> Bool Source #
Pretty Fixity' Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Fixity' -> Doc Source # prettyPrec :: Int -> Fixity' -> Doc Source # prettyList :: [Fixity'] -> Doc Source #
KillRange Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Fixity' Source #
LensFixity' Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods lensFixity' :: Lens' Fixity' Fixity' Source #
LensFixity Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods lensFixity :: Lens' Fixity Fixity' Source #
EmbPrj Fixity' Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Fixity' -> S Int32 Source # icod_ :: Fixity' -> S Int32 Source # value :: Int32 -> R Fixity' Source #
ToTerm Fixity' Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity' -> Term) Source # toTermR :: TCM (Fixity' -> ReduceM Term) Source #
PrimTerm Fixity' Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Fixity' -> TCM Term Source #

noFixity' :: Fixity' Source #

_fixityAssoc :: Lens' Associativity Fixity Source #

_fixityLevel :: Lens' FixityLevel Fixity Source #

class LensFixity a where Source #

Methods

lensFixity :: Lens' Fixity a Source #

Instances

LensFixity Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods lensFixity :: Lens' Fixity Fixity' Source #
LensFixity Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods lensFixity :: Lens' Fixity Fixity Source #
LensFixity QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity :: Lens' Fixity QName Source #
LensFixity Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity :: Lens' Fixity Name Source #
LensFixity NewNotation Source #
Instance details Defined in Agda.Syntax.Notation Methods lensFixity :: Lens' Fixity NewNotation Source #
LensFixity AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods lensFixity :: Lens' Fixity AbstractName Source #
LensFixity (ThingWithFixity a) Source #
Instance details Defined in Agda.Syntax.Fixity Methods lensFixity :: Lens' Fixity (ThingWithFixity a) Source #

class LensFixity' a where Source #

Methods

lensFixity' :: Lens' Fixity' a Source #

Instances

LensFixity' Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods lensFixity' :: Lens' Fixity' Fixity' Source #
LensFixity' QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity' :: Lens' Fixity' QName Source #
LensFixity' Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity' :: Lens' Fixity' Name Source #
LensFixity' (ThingWithFixity a) Source #
Instance details Defined in Agda.Syntax.Fixity Methods lensFixity' :: Lens' Fixity' (ThingWithFixity a) Source #

Import directive

data ImportDirective' n m Source #

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

Constructors

ImportDirective
Fields importDirRange :: Range using :: Using' n m hiding :: [ImportedName' n m] impRenaming :: [Renaming' n m] publicOpen :: Maybe Range 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 # (/=) :: ImportDirective' n m -> ImportDirective' n m -> Bool #
(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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportDirective' n m) # toConstr :: ImportDirective' n m -> Constr # dataTypeOf :: ImportDirective' n m -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportDirective' n m)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportDirective' n m)) # gmapT :: (forall b. Data b => b -> b) -> ImportDirective' n m -> ImportDirective' n m # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportDirective' n m -> r # gmapQ :: (forall d. Data d => d -> u) -> ImportDirective' n m -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportDirective' n m -> u # gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) # gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) # gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportDirective' n m -> m0 (ImportDirective' n m) #
(Show a, Show b) => Show (ImportDirective' a b) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ImportDirective' a b -> ShowS # show :: ImportDirective' a b -> String # showList :: [ImportDirective' a b] -> ShowS #
(NFData a, NFData b) => NFData (ImportDirective' a b) Source #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Common Methods rnf :: ImportDirective' a b -> () #
Null (ImportDirective' n m) Source #	`null` for import directives holds when everything is imported unchanged (no names are hidden or renamed).
Instance details Defined in Agda.Syntax.Common Methods empty :: ImportDirective' n m Source # null :: ImportDirective' n m -> Bool 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 #

defaultImportDir :: ImportDirective' n m Source #

Default is directive is private (use everything, but do not export).

isDefaultImportDir :: ImportDirective' n m -> Bool Source #

isDefaultImportDir implies null, but not the other way round.

data Using' n m Source #

The using clause of import directive.

Constructors

UseEverything	No `using` clause given.
Using [ImportedName' n m]	`using` the specified names.

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 # (/=) :: Using' n m -> Using' n m -> Bool #
(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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Using' n m) # toConstr :: Using' n m -> Constr # dataTypeOf :: Using' n m -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Using' n m)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Using' n m)) # gmapT :: (forall b. Data b => b -> b) -> Using' n m -> Using' n m # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using' n m -> r # gmapQ :: (forall d. Data d => d -> u) -> Using' n m -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Using' n m -> u # gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) # gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) # gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Using' n m -> m0 (Using' n m) #
(Show a, Show b) => Show (Using' a b) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Using' a b -> ShowS # show :: Using' a b -> String # showList :: [Using' a b] -> ShowS #
Semigroup (Using' n m) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Using' n m -> Using' n m -> Using' n m # sconcat :: NonEmpty (Using' n m) -> Using' n m # stimes :: Integral b => b -> Using' n m -> Using' n m #
Monoid (Using' n m) Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: Using' n m # mappend :: Using' n m -> Using' n m -> Using' n m # mconcat :: [Using' n m] -> Using' n m #
(NFData a, NFData b) => NFData (Using' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Using' a b -> () #
Null (Using' n m) Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Using' n m Source # null :: Using' n m -> Bool 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 #

mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2 Source #

data ImportedName' n m Source #

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

Constructors

ImportedModule m	Imported module name of type `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 # (/=) :: ImportedName' n m -> ImportedName' n m -> Bool #
(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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ImportedName' n m) # toConstr :: ImportedName' n m -> Constr # dataTypeOf :: ImportedName' n m -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ImportedName' n m)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ImportedName' n m)) # gmapT :: (forall b. Data b => b -> b) -> ImportedName' n m -> ImportedName' n m # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImportedName' n m -> r # gmapQ :: (forall d. Data d => d -> u) -> ImportedName' n m -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ImportedName' n m -> u # gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) # gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) # gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> ImportedName' n m -> m0 (ImportedName' n m) #
(Ord m, Ord n) => Ord (ImportedName' n m) Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: ImportedName' n m -> ImportedName' n m -> Ordering # (<) :: ImportedName' n m -> ImportedName' n m -> Bool # (<=) :: ImportedName' n m -> ImportedName' n m -> Bool # (>) :: ImportedName' n m -> ImportedName' n m -> Bool # (>=) :: ImportedName' n m -> ImportedName' n m -> Bool # max :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m # min :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m #
(Show m, Show n) => Show (ImportedName' n m) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ImportedName' n m -> ShowS # show :: ImportedName' n m -> String # showList :: [ImportedName' n m] -> ShowS #
(NFData a, NFData b) => NFData (ImportedName' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: ImportedName' a b -> () #
(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`. renFixity :: Maybe Fixity New fixity of `renTo` (optional). 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 # (/=) :: Renaming' n m -> Renaming' n m -> Bool #
(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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Renaming' n m) # toConstr :: Renaming' n m -> Constr # dataTypeOf :: Renaming' n m -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Renaming' n m)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Renaming' n m)) # gmapT :: (forall b. Data b => b -> b) -> Renaming' n m -> Renaming' n m # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' n m -> r # gmapQ :: (forall d. Data d => d -> u) -> Renaming' n m -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Renaming' n m -> u # gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) # gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) # gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> Renaming' n m -> m0 (Renaming' n m) #
(Show a, Show b) => Show (Renaming' a b) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Renaming' a b -> ShowS # show :: Renaming' a b -> String # showList :: [Renaming' a b] -> ShowS #
(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 -> () #
(Pretty a, Pretty b) => Pretty (Renaming' a b) Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Renaming' a b -> Doc Source # prettyPrec :: Int -> Renaming' a b -> Doc Source # prettyList :: [Renaming' a b] -> Doc 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 # (<$) :: a -> TerminationCheck b -> TerminationCheck a #
Eq m => Eq (TerminationCheck m) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: TerminationCheck m -> TerminationCheck m -> Bool # (/=) :: TerminationCheck m -> TerminationCheck m -> Bool #
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) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TerminationCheck m) # toConstr :: TerminationCheck m -> Constr # dataTypeOf :: TerminationCheck m -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TerminationCheck m)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TerminationCheck m)) # gmapT :: (forall b. Data b => b -> b) -> TerminationCheck m -> TerminationCheck m # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TerminationCheck m -> r # gmapQ :: (forall d. Data d => d -> u) -> TerminationCheck m -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TerminationCheck m -> u # gmapM :: Monad m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) # gmapMp :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) # gmapMo :: MonadPlus m0 => (forall d. Data d => d -> m0 d) -> TerminationCheck m -> m0 (TerminationCheck m) #
Show m => Show (TerminationCheck m) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> TerminationCheck m -> ShowS # show :: TerminationCheck m -> String # showList :: [TerminationCheck m] -> ShowS #
NFData a => NFData (TerminationCheck a) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: TerminationCheck a -> () #
KillRange m => KillRange (TerminationCheck m) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (TerminationCheck m) Source #

Positivity

data PositivityCheck Source #

Positivity check? (Default = True).

Constructors

YesPositivityCheck
NoPositivityCheck

Instances

Bounded PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods minBound :: PositivityCheck # maxBound :: PositivityCheck #
Enum PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: PositivityCheck -> PositivityCheck # pred :: PositivityCheck -> PositivityCheck # toEnum :: Int -> PositivityCheck # fromEnum :: PositivityCheck -> Int # enumFrom :: PositivityCheck -> [PositivityCheck] # enumFromThen :: PositivityCheck -> PositivityCheck -> [PositivityCheck] # enumFromTo :: PositivityCheck -> PositivityCheck -> [PositivityCheck] # enumFromThenTo :: PositivityCheck -> PositivityCheck -> PositivityCheck -> [PositivityCheck] #
Eq PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: PositivityCheck -> PositivityCheck -> Bool # (/=) :: PositivityCheck -> PositivityCheck -> Bool #
Data PositivityCheck 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) -> PositivityCheck -> c PositivityCheck # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PositivityCheck # toConstr :: PositivityCheck -> Constr # dataTypeOf :: PositivityCheck -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PositivityCheck) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PositivityCheck) # gmapT :: (forall b. Data b => b -> b) -> PositivityCheck -> PositivityCheck # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PositivityCheck -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PositivityCheck -> r # gmapQ :: (forall d. Data d => d -> u) -> PositivityCheck -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PositivityCheck -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PositivityCheck -> m PositivityCheck # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PositivityCheck -> m PositivityCheck # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PositivityCheck -> m PositivityCheck #
Ord PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: PositivityCheck -> PositivityCheck -> Ordering # (<) :: PositivityCheck -> PositivityCheck -> Bool # (<=) :: PositivityCheck -> PositivityCheck -> Bool # (>) :: PositivityCheck -> PositivityCheck -> Bool # (>=) :: PositivityCheck -> PositivityCheck -> Bool # max :: PositivityCheck -> PositivityCheck -> PositivityCheck # min :: PositivityCheck -> PositivityCheck -> PositivityCheck #
Show PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> PositivityCheck -> ShowS # show :: PositivityCheck -> String # showList :: [PositivityCheck] -> ShowS #
Semigroup PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: PositivityCheck -> PositivityCheck -> PositivityCheck # sconcat :: NonEmpty PositivityCheck -> PositivityCheck # stimes :: Integral b => b -> PositivityCheck -> PositivityCheck #
Monoid PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: PositivityCheck # mappend :: PositivityCheck -> PositivityCheck -> PositivityCheck # mconcat :: [PositivityCheck] -> PositivityCheck #
KillRange PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT PositivityCheck Source #

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 # maxBound :: UniverseCheck #
Enum UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: UniverseCheck -> UniverseCheck # pred :: UniverseCheck -> UniverseCheck # toEnum :: Int -> UniverseCheck # fromEnum :: UniverseCheck -> Int # enumFrom :: UniverseCheck -> [UniverseCheck] # enumFromThen :: UniverseCheck -> UniverseCheck -> [UniverseCheck] # enumFromTo :: UniverseCheck -> UniverseCheck -> [UniverseCheck] # enumFromThenTo :: UniverseCheck -> UniverseCheck -> UniverseCheck -> [UniverseCheck] #
Eq UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: UniverseCheck -> UniverseCheck -> Bool # (/=) :: UniverseCheck -> UniverseCheck -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UniverseCheck # toConstr :: UniverseCheck -> Constr # dataTypeOf :: UniverseCheck -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UniverseCheck) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UniverseCheck) # gmapT :: (forall b. Data b => b -> b) -> UniverseCheck -> UniverseCheck # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UniverseCheck -> r # gmapQ :: (forall d. Data d => d -> u) -> UniverseCheck -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> UniverseCheck -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UniverseCheck -> m UniverseCheck #
Ord UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: UniverseCheck -> UniverseCheck -> Ordering # (<) :: UniverseCheck -> UniverseCheck -> Bool # (<=) :: UniverseCheck -> UniverseCheck -> Bool # (>) :: UniverseCheck -> UniverseCheck -> Bool # (>=) :: UniverseCheck -> UniverseCheck -> Bool # max :: UniverseCheck -> UniverseCheck -> UniverseCheck # min :: UniverseCheck -> UniverseCheck -> UniverseCheck #
Show UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> UniverseCheck -> ShowS # show :: UniverseCheck -> String # showList :: [UniverseCheck] -> ShowS #
KillRange UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT UniverseCheck Source #

Universe checking

data CoverageCheck Source #

Coverage check? (Default is yes).

Constructors

YesCoverageCheck
NoCoverageCheck

Instances

Bounded CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods minBound :: CoverageCheck # maxBound :: CoverageCheck #
Enum CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: CoverageCheck -> CoverageCheck # pred :: CoverageCheck -> CoverageCheck # toEnum :: Int -> CoverageCheck # fromEnum :: CoverageCheck -> Int # enumFrom :: CoverageCheck -> [CoverageCheck] # enumFromThen :: CoverageCheck -> CoverageCheck -> [CoverageCheck] # enumFromTo :: CoverageCheck -> CoverageCheck -> [CoverageCheck] # enumFromThenTo :: CoverageCheck -> CoverageCheck -> CoverageCheck -> [CoverageCheck] #
Eq CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: CoverageCheck -> CoverageCheck -> Bool # (/=) :: CoverageCheck -> CoverageCheck -> Bool #
Data CoverageCheck 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) -> CoverageCheck -> c CoverageCheck # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoverageCheck # toConstr :: CoverageCheck -> Constr # dataTypeOf :: CoverageCheck -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoverageCheck) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoverageCheck) # gmapT :: (forall b. Data b => b -> b) -> CoverageCheck -> CoverageCheck # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoverageCheck -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoverageCheck -> r # gmapQ :: (forall d. Data d => d -> u) -> CoverageCheck -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CoverageCheck -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoverageCheck -> m CoverageCheck #
Ord CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: CoverageCheck -> CoverageCheck -> Ordering # (<) :: CoverageCheck -> CoverageCheck -> Bool # (<=) :: CoverageCheck -> CoverageCheck -> Bool # (>) :: CoverageCheck -> CoverageCheck -> Bool # (>=) :: CoverageCheck -> CoverageCheck -> Bool # max :: CoverageCheck -> CoverageCheck -> CoverageCheck # min :: CoverageCheck -> CoverageCheck -> CoverageCheck #
Show CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> CoverageCheck -> ShowS # show :: CoverageCheck -> String # showList :: [CoverageCheck] -> ShowS #
Semigroup CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck # sconcat :: NonEmpty CoverageCheck -> CoverageCheck # stimes :: Integral b => b -> CoverageCheck -> CoverageCheck #
Monoid CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: CoverageCheck # mappend :: CoverageCheck -> CoverageCheck -> CoverageCheck # mconcat :: [CoverageCheck] -> CoverageCheck #
KillRange CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT CoverageCheck Source #

Rewrite Directives on the LHS

data RewriteEqn' qn p e Source #

RewriteEqn' qn p e represents the rewrite and irrefutable with clauses of the LHS. qn stands for the QName of the auxiliary function generated to implement the feature p is the type of patterns e is the type of expressions

Constructors

Rewrite [(qn, e)]	rewrite e
Invert qn [(p, e)]	with p <- e

Instances

ToAbstract RewriteEqn (RewriteEqn' () Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RewriteEqn -> ScopeM (RewriteEqn' () Pattern Expr) Source #
ToConcrete RHS (RHS, [RewriteEqn], [WithHiding Expr], [Declaration]) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [RewriteEqn], [WithHiding Expr], [Declaration]) Source # bindToConcrete :: RHS -> ((RHS0, [RewriteEqn], [WithHiding Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b Source #
Functor (RewriteEqn' qn p) Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> RewriteEqn' qn p a -> RewriteEqn' qn p b # (<$) :: a -> RewriteEqn' qn p b -> RewriteEqn' qn p a #
Foldable (RewriteEqn' qn p) Source #
Instance details Defined in Agda.Syntax.Common Methods fold :: Monoid m => RewriteEqn' qn p m -> m # foldMap :: Monoid m => (a -> m) -> RewriteEqn' qn p a -> m # foldr :: (a -> b -> b) -> b -> RewriteEqn' qn p a -> b # foldr' :: (a -> b -> b) -> b -> RewriteEqn' qn p a -> b # foldl :: (b -> a -> b) -> b -> RewriteEqn' qn p a -> b # foldl' :: (b -> a -> b) -> b -> RewriteEqn' qn p a -> b # foldr1 :: (a -> a -> a) -> RewriteEqn' qn p a -> a # foldl1 :: (a -> a -> a) -> RewriteEqn' qn p a -> a # toList :: RewriteEqn' qn p a -> [a] # null :: RewriteEqn' qn p a -> Bool # length :: RewriteEqn' qn p a -> Int # elem :: Eq a => a -> RewriteEqn' qn p a -> Bool # maximum :: Ord a => RewriteEqn' qn p a -> a # minimum :: Ord a => RewriteEqn' qn p a -> a # sum :: Num a => RewriteEqn' qn p a -> a # product :: Num a => RewriteEqn' qn p a -> a #
Traversable (RewriteEqn' qn p) Source #
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> RewriteEqn' qn p a -> f (RewriteEqn' qn p b) # sequenceA :: Applicative f => RewriteEqn' qn p (f a) -> f (RewriteEqn' qn p a) # mapM :: Monad m => (a -> m b) -> RewriteEqn' qn p a -> m (RewriteEqn' qn p b) # sequence :: Monad m => RewriteEqn' qn p (m a) -> m (RewriteEqn' qn p a) #
(Eq qn, Eq e, Eq p) => Eq (RewriteEqn' qn p e) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: RewriteEqn' qn p e -> RewriteEqn' qn p e -> Bool # (/=) :: RewriteEqn' qn p e -> RewriteEqn' qn p e -> Bool #
(Data qn, Data p, Data e) => Data (RewriteEqn' qn p e) Source #
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) -> RewriteEqn' qn p e -> c (RewriteEqn' qn p e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RewriteEqn' qn p e) # toConstr :: RewriteEqn' qn p e -> Constr # dataTypeOf :: RewriteEqn' qn p e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RewriteEqn' qn p e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RewriteEqn' qn p e)) # gmapT :: (forall b. Data b => b -> b) -> RewriteEqn' qn p e -> RewriteEqn' qn p e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RewriteEqn' qn p e -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RewriteEqn' qn p e -> r # gmapQ :: (forall d. Data d => d -> u) -> RewriteEqn' qn p e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RewriteEqn' qn p e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) #
(Show qn, Show e, Show p) => Show (RewriteEqn' qn p e) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> RewriteEqn' qn p e -> ShowS # show :: RewriteEqn' qn p e -> String # showList :: [RewriteEqn' qn p e] -> ShowS #
(NFData qn, NFData p, NFData e) => NFData (RewriteEqn' qn p e) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: RewriteEqn' qn p e -> () #
(Pretty p, Pretty e) => Pretty (RewriteEqn' qn p e) Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: RewriteEqn' qn p e -> Doc Source # prettyPrec :: Int -> RewriteEqn' qn p e -> Doc Source # prettyList :: [RewriteEqn' qn p e] -> Doc Source #
(KillRange qn, KillRange e, KillRange p) => KillRange (RewriteEqn' qn p e) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (RewriteEqn' qn p e) Source #
(HasRange qn, HasRange p, HasRange e) => HasRange (RewriteEqn' qn p e) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: RewriteEqn' qn p e -> Range Source #
(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn p e) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> RewriteEqn' qn p e -> RewriteEqn' qn p e Source # traverseExpr :: Monad m => (Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source # foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn p e -> m Source #
(AllNames qn, AllNames e) => AllNames (RewriteEqn' qn p e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods allNames :: RewriteEqn' qn p e -> Seq QName Source #
(ExprLike qn, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn p e) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source # foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn p e -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> RewriteEqn' qn p e -> m (RewriteEqn' qn p e) Source # mapExpr :: (Expr -> Expr) -> RewriteEqn' qn p e -> RewriteEqn' qn p e Source #
ToAbstract (RewriteEqn' () Pattern Expr) RewriteEqn Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RewriteEqn' () Pattern Expr -> ScopeM RewriteEqn Source #
(ToConcrete p q, ToConcrete a b) => ToConcrete (RewriteEqn' qn p a) (RewriteEqn' () q b) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RewriteEqn' qn p a -> AbsToCon (RewriteEqn' () q b) Source # bindToConcrete :: RewriteEqn' qn p a -> (RewriteEqn' () q b -> AbsToCon b0) -> AbsToCon b0 Source #

Information on expanded ellipsis (`...`)

data ExpandedEllipsis Source #

Constructors

ExpandedEllipsis
Fields ellipsisRange :: Range ellipsisWithArgs :: Int
NoEllipsis

Instances

Eq ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool # (/=) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool #
Data ExpandedEllipsis 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) -> ExpandedEllipsis -> c ExpandedEllipsis # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExpandedEllipsis # toConstr :: ExpandedEllipsis -> Constr # dataTypeOf :: ExpandedEllipsis -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExpandedEllipsis) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpandedEllipsis) # gmapT :: (forall b. Data b => b -> b) -> ExpandedEllipsis -> ExpandedEllipsis # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExpandedEllipsis -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExpandedEllipsis -> r # gmapQ :: (forall d. Data d => d -> u) -> ExpandedEllipsis -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ExpandedEllipsis -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandedEllipsis -> m ExpandedEllipsis #
Show ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ExpandedEllipsis -> ShowS # show :: ExpandedEllipsis -> String # showList :: [ExpandedEllipsis] -> ShowS #
NFData ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: ExpandedEllipsis -> () #
Null ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: ExpandedEllipsis Source # null :: ExpandedEllipsis -> Bool Source #
KillRange ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ExpandedEllipsis Source #
EmbPrj ExpandedEllipsis Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: ExpandedEllipsis -> S Int32 Source # icod_ :: ExpandedEllipsis -> S Int32 Source # value :: Int32 -> R ExpandedEllipsis Source #

type Notation = [GenPart] Source #

Notation as provided by the syntax declaration.

noNotation :: Notation Source #

data GenPart Source #

Part of a Notation

Constructors

BindHole Range (Ranged Int)	Argument is the position of the hole (with binding) where the binding should occur. First range is the rhs range and second is the binder.
NormalHole Range (NamedArg (Ranged Int))	Argument is where the expression should go.
WildHole (Ranged Int)	An underscore in binding position.
IdPart RString

Instances

Eq GenPart Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: GenPart -> GenPart -> Bool # (/=) :: GenPart -> GenPart -> Bool #
Data GenPart 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) -> GenPart -> c GenPart # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenPart # toConstr :: GenPart -> Constr # dataTypeOf :: GenPart -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GenPart) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenPart) # gmapT :: (forall b. Data b => b -> b) -> GenPart -> GenPart # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r # gmapQ :: (forall d. Data d => d -> u) -> GenPart -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> GenPart -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart #
Ord GenPart Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: GenPart -> GenPart -> Ordering # (<) :: GenPart -> GenPart -> Bool # (<=) :: GenPart -> GenPart -> Bool # (>) :: GenPart -> GenPart -> Bool # (>=) :: GenPart -> GenPart -> Bool # max :: GenPart -> GenPart -> GenPart # min :: GenPart -> GenPart -> GenPart #
Show GenPart Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> GenPart -> ShowS # show :: GenPart -> String # showList :: [GenPart] -> ShowS #
NFData GenPart Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: GenPart -> () #
Pretty GenPart Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: GenPart -> Doc Source # prettyPrec :: Int -> GenPart -> Doc Source # prettyList :: [GenPart] -> Doc Source #
KillRange GenPart Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT GenPart Source #
SetRange GenPart Source #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> GenPart -> GenPart Source #
HasRange GenPart Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: GenPart -> Range Source #
EmbPrj GenPart Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: GenPart -> S Int32 Source # icod_ :: GenPart -> S Int32 Source # value :: Int32 -> R GenPart Source #

Documentation

Delayed

File

Eta-equality

Induction

Hiding

Modalities

Quantities

Quantity origin.

Instances for Q0Origin.

Instances for Q1Origin.

Instances for QωOrigin.

Quantity.

Relevance

Cohesion

Origin of arguments (user-written, inserted or reflected)

Free variable annotations

Argument decoration

Arguments

Names

Named arguments

ArgName

Range decoration.

Raw names (before parsing into name parts).

Further constructor and projection info

Infixity, access, abstract, etc.

private blocks, public imports

abstract blocks

instance blocks

macro blocks

NameId

Meta variables

Placeholders (used to parse sections)

Interaction meta variables

Fixity

Notation coupled with Fixity

Import directive

HasRange instances

KillRange instances

NFData instances

Termination

Positivity

Universe checking

Universe checking

Rewrite Directives on the LHS

Information on expanded ellipsis (...)

Instances for `Q0Origin`.

Instances for `Q1Origin`.

Instances for `QωOrigin`.

Notation coupled with `Fixity`

Information on expanded ellipsis (`...`)