Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Common

Contents

Orphan instances

Description

Some common syntactic entities are defined in this module.

Synopsis

data Hiding
- = Hidden
- | Instance Overlappable
- | NotHidden
data Arg e = Arg {
- argInfo :: ArgInfo
- unArg :: e
}
type Nat = Int
newtype InteractionId = InteractionId {
- interactionId :: Nat
}
data Modality = Modality {
- modRelevance :: Relevance
- modQuantity :: Quantity
- modCohesion :: Cohesion
}
newtype ProblemId = ProblemId Nat
data Fixity = Fixity {
- fixityRange :: Range
- fixityLevel :: !FixityLevel
- fixityAssoc :: !Associativity
}
data MetaId = MetaId {
- metaId :: !Word64
- metaModule :: !ModuleNameHash
}
data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
}
data TerminationCheck m
- = TerminationCheck
- | NoTerminationCheck
- | NonTerminating
- | Terminating
- | TerminationMeasure Range m
type Notation = [NotationPart]
data Lock
- = IsNotLock
- | IsLock LockOrigin
data Cubical
- = CErased
- | CFull
type NamedArg a = Arg (Named_ a)
data ImportedName' n m
- = ImportedModule m
- | ImportedName n
data ConOrigin
- = ConOSystem
- | ConOCon
- | ConORec
- | ConOSplit
data ProjOrigin
- = ProjPrefix
- | ProjPostfix
- | ProjSystem
data Relevance
- = Relevant
- | NonStrict
- | Irrelevant
data NameId = NameId !Word64 !ModuleNameHash
data WithHiding a = WithHiding {
- whHiding :: !Hiding
- whThing :: a
}
data Associativity
- = NonAssoc
- | LeftAssoc
- | RightAssoc
newtype Constr a = Constr a
data Overlappable
- = YesOverlap
- | NoOverlap
type Arity = Nat
data FileType
- = AgdaFileType
- | MdFileType
- | RstFileType
- | TexFileType
- | OrgFileType
- | TypstFileType
data Language
- = WithoutK
- | WithK
- | Cubical Cubical
data RecordDirectives' a = RecordDirectives {
- recInductive :: Maybe (Ranged Induction)
- recHasEta :: Maybe HasEta0
- recPattern :: Maybe Range
- recConstructor :: Maybe a
}
type HasEta0 = HasEta' ()
data HasEta' a
- = YesEta
- | NoEta a
type HasEta = HasEta' PatternOrCopattern
data PatternOrCopattern
- = PatternMatching
- | CopatternMatching
class PatternMatchingAllowed a where
- patternMatchingAllowed :: a -> Bool
class CopatternMatchingAllowed a where
- copatternMatchingAllowed :: a -> Bool
class LensHiding a where
- getHiding :: a -> Hiding
- setHiding :: Hiding -> a -> a
- mapHiding :: (Hiding -> Hiding) -> a -> a
class LensArgInfo a where
- getArgInfo :: a -> ArgInfo
- setArgInfo :: ArgInfo -> a -> a
- mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a
data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
}
newtype UnderAddition t = UnderAddition t
newtype UnderComposition t = UnderComposition t
data Quantity
- = Quantity0 Q0Origin
- | Quantity1 Q1Origin
- | Quantityω QωOrigin
data Cohesion
- = Flat
- | Continuous
- | Squash
class LensModality a where
- getModality :: a -> Modality
- setModality :: Modality -> a -> a
- mapModality :: (Modality -> Modality) -> a -> a
class LensRelevance a where
- getRelevance :: a -> Relevance
- setRelevance :: Relevance -> a -> a
- mapRelevance :: (Relevance -> Relevance) -> a -> a
class LensQuantity a where
- getQuantity :: a -> Quantity
- setQuantity :: Quantity -> a -> a
- mapQuantity :: (Quantity -> Quantity) -> a -> a
class LensCohesion a where
- getCohesion :: a -> Cohesion
- setCohesion :: Cohesion -> a -> a
- mapCohesion :: (Cohesion -> Cohesion) -> a -> 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 Erased
- = Erased Q0Origin
- | NotErased QωOrigin
data Annotation = Annotation {
- annLock :: Lock
}
class LensAnnotation a where
- getAnnotation :: a -> Annotation
- setAnnotation :: Annotation -> a -> a
- mapAnnotation :: (Annotation -> Annotation) -> a -> a
data LockOrigin
- = LockOLock
- | LockOTick
class LensLock a where
- getLock :: a -> Lock
- setLock :: Lock -> a -> a
- mapLock :: (Lock -> Lock) -> a -> a
data ArgInfo = ArgInfo {
- argInfoHiding :: Hiding
- argInfoModality :: Modality
- argInfoOrigin :: Origin
- argInfoFreeVariables :: FreeVariables
- argInfoAnnotation :: Annotation
}
data Origin
- = UserWritten
- | Inserted
- | Reflected
- | CaseSplit
- | Substitution
- | ExpandedPun
- | Generalization
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
class LensFreeVariables a where
- getFreeVariables :: a -> FreeVariables
- setFreeVariables :: FreeVariables -> a -> a
- mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a
class Eq a => Underscore a where
- underscore :: a
- isUnderscore :: a -> Bool
type Named_ = Named NamedName
type NamedName = WithOrigin (Ranged ArgName)
type ArgName = String
class LensNamed a where
- type NameOf a
- lensNamed :: Lens' a (Maybe (NameOf a))
type RawName = String
type RString = Ranged RawName
data IsInfix
- = InfixDef
- | PrefixDef
data Access
- = PrivateAccess Origin
- | PublicAccess
data IsAbstract
- = AbstractDef
- | ConcreteDef
class LensIsAbstract a where
- lensIsAbstract :: Lens' a IsAbstract
class AnyIsAbstract a where
- anyIsAbstract :: a -> IsAbstract
data IsInstance
- = InstanceDef Range
- | NotInstanceDef
data IsMacro
- = MacroDef
- | NotMacroDef
data IsOpaque
- = OpaqueDef !OpaqueId
- | TransparentDef
data OpaqueId = OpaqueId !Word64 !ModuleNameHash
class LensIsOpaque a where
- lensIsOpaque :: Lens' a IsOpaque
data JointOpacity
- = UniqueOpaque !OpaqueId
- | DifferentOpaque !(HashSet OpaqueId)
- | NoOpaque
class AllAreOpaque a where
- jointOpacity :: a -> JointOpacity
data PositionInName
- = Beginning
- | Middle
- | End
data MaybePlaceholder e
- = Placeholder !PositionInName
- | NoPlaceholder !(Maybe PositionInName) e
type PrecedenceLevel = Double
data FixityLevel
- = Unrelated
- | Related !PrecedenceLevel
data Fixity' = Fixity' {
- theFixity :: !Fixity
- theNotation :: Notation
- theNameRange :: Range
}
class LensFixity a where
- lensFixity :: Lens' a Fixity
class LensFixity' a where
- lensFixity' :: Lens' a Fixity'
data ImportDirective' n m = ImportDirective {
- importDirRange :: Range
- using :: Using' n m
- hiding :: HidingDirective' n m
- impRenaming :: RenamingDirective' n m
- publicOpen :: Maybe Range
}
data Using' n m
- = UseEverything
- | Using [ImportedName' n m]
type HidingDirective' n m = [ImportedName' n m]
type RenamingDirective' n m = [Renaming' n m]
data Renaming' n m = Renaming {
- renFrom :: ImportedName' n m
- renTo :: ImportedName' n m
- renFixity :: Maybe Fixity
- renToRange :: Range
}
data PositivityCheck
- = YesPositivityCheck
- | NoPositivityCheck
data UniverseCheck
- = YesUniverseCheck
- | NoUniverseCheck
data CoverageCheck
- = YesCoverageCheck
- | NoCoverageCheck
data RewriteEqn' qn nm p e
- = Rewrite (List1 (qn, e))
- | Invert qn (List1 (Named nm (p, e)))
data ExpandedEllipsis
- = ExpandedEllipsis {
  - ellipsisRange :: Range
  - ellipsisWithArgs :: Int
  }
- | NoEllipsis
data NotationPart
- = IdPart RString
- | HolePart Range (NamedArg (Ranged Int))
- | VarPart Range (Ranged BoundVariablePosition)
- | WildPart (Ranged BoundVariablePosition)
data BoundVariablePosition = BoundVariablePosition {
- holeNumber :: !Int
- varNumber :: !Int
}
fromImportedName :: ImportedName' a a -> a
partitionImportedNames :: [ImportedName' n m] -> ([n], [m])
defaultArgInfo :: ArgInfo
defaultArg :: a -> Arg a
hasQuantity0 :: LensQuantity a => a -> Bool
defaultFixity :: Fixity
isInstance :: LensHiding a => a -> Bool
emptyRecordDirectives :: RecordDirectives' a
hidingToString :: Hiding -> String
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
sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool
composeModality :: Modality -> Modality -> Modality
unitModality :: Modality
inverseComposeModality :: Modality -> Modality -> Modality
addModality :: Modality -> Modality -> Modality
zeroModality :: Modality
moreUsableModality :: Modality -> Modality -> Bool
usableModality :: LensModality a => a -> Bool
usableRelevance :: LensRelevance a => a -> Bool
usableQuantity :: LensQuantity a => a -> Bool
usableCohesion :: LensCohesion a => a -> Bool
composeRelevance :: Relevance -> Relevance -> Relevance
composeQuantity :: Quantity -> Quantity -> Quantity
composeCohesion :: Cohesion -> Cohesion -> Cohesion
applyModality :: LensModality a => Modality -> a -> a
inverseComposeRelevance :: Relevance -> Relevance -> Relevance
inverseComposeQuantity :: Quantity -> Quantity -> Quantity
inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion
inverseApplyModalityButNotQuantity :: LensModality a => Modality -> a -> a
addRelevance :: Relevance -> Relevance -> Relevance
addQuantity :: Quantity -> Quantity -> Quantity
addCohesion :: Cohesion -> Cohesion -> Cohesion
zeroRelevance :: Relevance
zeroQuantity :: Quantity
zeroCohesion :: Cohesion
unitRelevance :: Relevance
unitQuantity :: Quantity
unitCohesion :: Cohesion
topModality :: Modality
topRelevance :: Relevance
topQuantity :: Quantity
topCohesion :: Cohesion
defaultModality :: Modality
defaultRelevance :: Relevance
defaultQuantity :: Quantity
defaultCohesion :: Cohesion
sameModality :: (LensModality a, LensModality b) => a -> b -> Bool
sameRelevance :: Relevance -> Relevance -> Bool
sameQuantity :: Quantity -> Quantity -> Bool
sameCohesion :: Cohesion -> Cohesion -> Bool
lModRelevance :: Lens' Modality Relevance
lModQuantity :: Lens' Modality Quantity
lModCohesion :: Lens' Modality Cohesion
getRelevanceMod :: LensModality a => LensGet a Relevance
setRelevanceMod :: LensModality a => LensSet a Relevance
mapRelevanceMod :: LensModality a => LensMap a Relevance
getQuantityMod :: LensModality a => LensGet a Quantity
setQuantityMod :: LensModality a => LensSet a Quantity
mapQuantityMod :: LensModality a => LensMap a Quantity
getCohesionMod :: LensModality a => LensGet a Cohesion
setCohesionMod :: LensModality a => LensSet a Cohesion
mapCohesionMod :: LensModality a => LensMap a Cohesion
moreQuantity :: Quantity -> Quantity -> Bool
applyQuantity :: LensQuantity a => Quantity -> a -> a
inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a
hasQuantity1 :: LensQuantity a => a -> Bool
hasQuantityω :: LensQuantity a => a -> Bool
noUserQuantity :: LensQuantity a => a -> Bool
defaultErased :: Erased
asQuantity :: Erased -> Quantity
erasedFromQuantity :: Quantity -> Maybe Erased
sameErased :: Erased -> Erased -> Bool
isErased :: Erased -> Bool
composeErased :: Erased -> Erased -> Erased
allRelevances :: [Relevance]
isRelevant :: LensRelevance a => a -> Bool
isIrrelevant :: LensRelevance a => a -> Bool
isNonStrict :: LensRelevance a => a -> Bool
moreRelevant :: Relevance -> Relevance -> Bool
applyRelevance :: LensRelevance a => Relevance -> a -> a
inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a
irrToNonStrict :: Relevance -> Relevance
nonStrictToRel :: Relevance -> Relevance
nonStrictToIrr :: Relevance -> Relevance
defaultAnnotation :: Annotation
defaultLock :: Lock
allCohesions :: [Cohesion]
moreCohesion :: Cohesion -> Cohesion -> Bool
applyCohesion :: LensCohesion a => Cohesion -> a -> a
inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a
unknownFreeVariables :: FreeVariables
noFreeVariables :: FreeVariables
oneFreeVariable :: Int -> FreeVariables
freeVariablesFromList :: [Int] -> FreeVariables
hasNoFreeVariables :: LensFreeVariables a => a -> Bool
getHidingArgInfo :: LensArgInfo a => LensGet a Hiding
setHidingArgInfo :: LensArgInfo a => LensSet a Hiding
mapHidingArgInfo :: LensArgInfo a => LensMap a Hiding
getModalityArgInfo :: LensArgInfo a => LensGet a Modality
setModalityArgInfo :: LensArgInfo a => LensSet a Modality
mapModalityArgInfo :: LensArgInfo a => LensMap a Modality
getOriginArgInfo :: LensArgInfo a => LensGet a Origin
setOriginArgInfo :: LensArgInfo a => LensSet a Origin
mapOriginArgInfo :: LensArgInfo a => LensMap a Origin
getFreeVariablesArgInfo :: LensArgInfo a => LensGet a FreeVariables
setFreeVariablesArgInfo :: LensArgInfo a => LensSet a FreeVariables
mapFreeVariablesArgInfo :: LensArgInfo a => LensMap a FreeVariables
isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool
withArgsFrom :: [a] -> [Arg b] -> [Arg a]
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a]
sameName :: NamedName -> NamedName -> Bool
unnamed :: a -> Named name a
isUnnamed :: Named name a -> Maybe a
named :: name -> a -> Named name a
userNamed :: Ranged ArgName -> a -> Named_ a
getNameOf :: LensNamed a => a -> Maybe (NameOf a)
setNameOf :: LensNamed a => Maybe (NameOf a) -> a -> a
mapNameOf :: LensNamed a => (Maybe (NameOf a) -> Maybe (NameOf a)) -> a -> a
bareNameOf :: (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameWithDefault :: (LensNamed a, NameOf a ~ NamedName) => ArgName -> a -> ArgName
namedSame :: (LensNamed a, LensNamed b, NameOf a ~ NamedName, NameOf b ~ NamedName) => a -> b -> Bool
fittingNamedArg :: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) => arg -> dom -> Maybe Bool
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
argNameToString :: ArgName -> String
stringToArgName :: String -> ArgName
appendArgNames :: ArgName -> ArgName -> ArgName
unranged :: a -> Ranged a
rawNameToString :: RawName -> String
stringToRawName :: String -> RawName
bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin
noPlaceholder :: e -> MaybePlaceholder e
noFixity :: Fixity
noFixity' :: Fixity'
noNotation :: Notation
_fixityAssoc :: Lens' Fixity Associativity
_fixityLevel :: Lens' Fixity FixityLevel
defaultImportDir :: ImportDirective' n m
isDefaultImportDir :: ImportDirective' n m -> Bool
mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2
setImportedName :: ImportedName' a a -> a -> ImportedName' a a
module Agda.Syntax.TopLevelModuleName.Boot
data Induction
- = Inductive
- | CoInductive

Documentation

data Hiding Source #

Constructors

Hidden
Instance Overlappable
NotHidden

Instances

Instances details

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 #
Pretty Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: Hiding -> Doc Source # prettyPrec :: Int -> Hiding -> Doc Source # prettyList :: [Hiding] -> Doc Source #
HasRange Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Hiding -> Range Source #
KillRange Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Hiding Source #
Verbalize Hiding Source #
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Hiding -> String Source #
ChooseFlex Hiding Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Hiding -> Hiding -> FlexChoice 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 #
Unquote Hiding Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Hiding Source #
Monoid Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: Hiding mappend :: Hiding -> Hiding -> Hiding mconcat :: [Hiding] -> Hiding
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
Show Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Hiding -> ShowS show :: Hiding -> String showList :: [Hiding] -> ShowS
NFData Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Hiding -> ()
Eq Hiding Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Hiding -> Hiding -> Bool (/=) :: Hiding -> Hiding -> Bool
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
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 Arg e Source #

Constructors

Arg
Fields argInfo :: ArgInfo unArg :: e

Instances

Instances details

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 #
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 #
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 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)
Functor Arg Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> Arg a -> Arg b (<$) :: a -> Arg b -> Arg a #
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 Term (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (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 Args (MM (ArgList O) (RefInfo O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) 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 #
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 #
Conversion MOT (Exp O) Term Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term Source #
Conversion MOT (Exp O) Type Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type 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 [Clause] [([Pat O], MExp O)] Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp 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 #
SubstExpr a => SubstExpr (Arg a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Arg a -> Arg a Source #
IsProjP a => IsProjP (Arg a) Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source #
APatternLike a => APatternLike (Arg a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (Arg a) Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (Arg a)) -> m -> m) -> Arg a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (Arg a)) -> m (Pattern' (ADotT (Arg a)))) -> (Pattern' (ADotT (Arg a)) -> m (Pattern' (ADotT (Arg a)))) -> Arg a -> m (Arg a) Source #
DeclaredNames a => DeclaredNames (Arg a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Arg a -> m Source #
ExprLike a => ExprLike (Arg a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Arg a) Source # foldExpr :: FoldExprFn m (Arg a) Source # traverseExpr :: TraverseExprFn m (Arg a) Source # mapExpr :: (Expr -> Expr) -> Arg a -> Arg a Source #
LensAnnotation (Arg t) Source #
Instance details Defined in Agda.Syntax.Common Methods getAnnotation :: Arg t -> Annotation Source # setAnnotation :: Annotation -> Arg t -> Arg t Source # mapAnnotation :: (Annotation -> Annotation) -> Arg t -> Arg t 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 #
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 #
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 #
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 #
LensLock (Arg t) Source #
Instance details Defined in Agda.Syntax.Common Methods getLock :: Arg t -> Lock Source # setLock :: Lock -> Arg t -> Arg t Source # mapLock :: (Lock -> Lock) -> Arg t -> Arg t 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 #
LensNamed a => LensNamed (Arg a) Source #
Instance details Defined in Agda.Syntax.Common Associated Types type NameOf (Arg a) Source # Methods lensNamed :: Lens' (Arg a) (Maybe (NameOf (Arg a))) 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 #
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 #
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 #
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 #
ExprLike a => ExprLike (Arg a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Arg a -> Arg a Source # foldExpr :: Monoid m => (Expr -> m) -> Arg a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Arg a -> m (Arg a) 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 #
LensSort a => LensSort (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' (Arg a) Sort Source # getSort :: Arg a -> Sort Source #
PatternVars (Arg (Pattern' a)) Source #
Instance details Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (Arg (Pattern' a)) Source # Methods patternVars :: Arg (Pattern' a) -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)] Source #
PatternVars (NamedArg (Pattern' a)) Source #
Instance details Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (NamedArg (Pattern' a)) Source # Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source #
GetDefs a => GetDefs (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Arg a -> m () 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 #
AllMetas a => AllMetas (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal.MetaVars Methods allMetas :: Monoid m => (MetaId -> m) -> Arg a -> m Source #
NamesIn a => NamesIn (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Arg a -> m Source #
CountPatternVars a => CountPatternVars (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Arg a -> Int Source #
PatternVarModalities a => PatternVarModalities (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern Associated Types type PatVar (Arg a) Source # Methods patternVarModalities :: Arg a -> [(PatVar (Arg a), Modality)] Source #
HasRange a => HasRange (Arg a) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Arg a -> Range 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 #
ToConcrete a => ToConcrete (Arg a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Arg a) Source # Methods toConcrete :: Arg a -> AbsToCon (ConOfAbs (Arg a)) Source # bindToConcrete :: Arg a -> (ConOfAbs (Arg a) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract c => ToAbstract (Arg c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Arg c) Source # Methods toAbstract :: Arg c -> ScopeM (AbsOfCon (Arg c)) Source #
Reify i => Reify (Arg i) Source #	Skip reification of implicit and irrelevant args if option is off.
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (Arg i) Source # Methods reify :: MonadReify m => Arg i -> m (ReifiesTo (Arg i)) Source # reifyWhen :: MonadReify m => Bool -> Arg i -> m (ReifiesTo (Arg i)) Source #
ToAbstract r => ToAbstract (Arg r) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Arg r) Source # Methods toAbstract :: MonadReflectedToAbstract m => Arg r -> m (AbsOfRef (Arg r)) Source #
ToAbstract r => ToAbstract [Arg r] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef [Arg r] Source # Methods toAbstract :: MonadReflectedToAbstract m => [Arg r] -> m (AbsOfRef [Arg r]) Source #
AbsTerm a => AbsTerm (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Arg a -> 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 #
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 #
PrecomputeFreeVars a => PrecomputeFreeVars (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Arg a -> FV (Arg a) Source #
(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)
UsableModality a => UsableModality (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Arg a -> m Bool Source #
UsableRelevance a => UsableRelevance (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Arg a -> m Bool Source #
NoProjectedVar a => NoProjectedVar (Arg a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Arg a -> Either ProjectedVar () Source #
ReduceAndEtaContract a => ReduceAndEtaContract (Arg a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: 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 #
AnyRigid a => AnyRigid (Arg a) Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods anyRigid :: PureTCM 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 #
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 #
ComputeOccurrences a => ComputeOccurrences (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Arg a -> OccM OccurrencesBuilder Source #
PrettyTCM (Arg Expr) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Expr -> m Doc Source #
PrettyTCM (Arg Term) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Term -> m Doc Source #
PrettyTCM (Arg Type) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Type -> m Doc Source #
PrettyTCM (Arg Bool) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Bool -> m Doc Source #
PrettyTCM (NamedArg Expr) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc Source #
PrettyTCM (NamedArg Term) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Term -> m Doc Source #
NormaliseProjP a => NormaliseProjP (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Arg a -> m (Arg a) Source #
Instantiate t => Instantiate (Arg t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Arg t -> ReduceM (Arg t) Source #
InstantiateFull t => InstantiateFull (Arg t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Arg t -> ReduceM (Arg t) Source #
IsMeta a => IsMeta (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Arg a -> Maybe MetaId Source #
Normalise t => Normalise (Arg t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: 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 #
Simplify t => Simplify (Arg t) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Arg t -> ReduceM (Arg t)
GetMatchables a => GetMatchables (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Arg a -> [QName] Source #
IsFlexiblePattern a => IsFlexiblePattern (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Arg a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Arg a -> m Bool 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 #
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 #
Subst a => Subst (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg (Arg a) Source # Methods applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a 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)
PiApplyM a => PiApplyM (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Arg a -> m Type Source # piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Arg a -> m Type Source #
IApplyVars p => IApplyVars (NamedArg p) Source #
Instance details Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source #
Unquote a => Unquote (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM (Arg a) Source #
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 -> ()
Eq e => Eq (Arg e) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Arg e -> Arg e -> Bool (/=) :: Arg e -> Arg e -> Bool
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
LabelPatVars a b => LabelPatVars (Arg a) (Arg b) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern Associated Types type PatVarLabel (Arg b) Source # Methods labelPatVars :: Arg a -> State [PatVarLabel (Arg b)] (Arg b) Source # unlabelPatVars :: Arg b -> Arg a 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 #
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: Arg DeBruijnPattern -> Elim' NLPat Source #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
Match a b => Match (Arg a) (Arg b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> TypeOf (Arg b) -> Arg a -> Arg b -> NLM () Source #
NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => Arg p -> m (Arg a) Source #
PatternFrom a b => PatternFrom (Arg a) (Arg b) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf (Arg a) -> Arg a -> TCM (Arg b) Source #
AddContext (List1 (Arg Name), Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (Arg Name), Type) -> m a -> m a Source # contextSize :: (List1 (Arg Name), Type) -> Nat Source #
AddContext (List1 (NamedArg Name), Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # contextSize :: (List1 (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 #
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 #
type ADotT (Arg a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern type ADotT (Arg a) = ADotT a
type NameOf (Arg a) Source #
Instance details Defined in Agda.Syntax.Common type NameOf (Arg a) = NameOf a
type PatternVarOut (Arg (Pattern' a)) Source #
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (Arg (Pattern' a)) = a
type PatternVarOut (NamedArg (Pattern' a)) Source #
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (NamedArg (Pattern' a)) = a
type TypeOf (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal type TypeOf (Arg a) = Dom (TypeOf a)
type PatVar (Arg a) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVar (Arg a) = PatVar a
type PatVarLabel (Arg b) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel (Arg b) = PatVarLabel b
type ConOfAbs (Arg a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Arg a) = Arg (ConOfAbs a)
type AbsOfCon (Arg c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Arg c) = Arg (AbsOfCon c)
type ReifiesTo (Arg i) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Arg i) = Arg (ReifiesTo i)
type AbsOfRef (Arg r) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Arg r) = NamedArg (AbsOfRef r)
type AbsOfRef [Arg r] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef [Arg r] = [NamedArg (AbsOfRef r)]
type SubstArg (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Arg a) = SubstArg a

type Nat = Int Source #

newtype InteractionId Source #

Constructors

InteractionId
Fields interactionId :: Nat

Instances

Instances details

EncodeTCM InteractionId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: InteractionId -> TCM Value Source #
Pretty InteractionId Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: InteractionId -> Doc Source # prettyPrec :: Int -> InteractionId -> Doc Source # prettyList :: [InteractionId] -> Doc Source #
KillRange InteractionId Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT InteractionId Source #
ToConcrete InteractionId Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs InteractionId Source # Methods toConcrete :: InteractionId -> AbsToCon (ConOfAbs InteractionId) Source # bindToConcrete :: InteractionId -> (ConOfAbs InteractionId -> AbsToCon b) -> AbsToCon b Source #
HasFresh InteractionId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' TCState InteractionId Source # nextFresh' :: InteractionId -> InteractionId Source #
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]
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
Read InteractionId
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS InteractionId readList :: ReadS [InteractionId] readPrec :: ReadPrec InteractionId readListPrec :: ReadPrec [InteractionId]
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
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
NFData InteractionId Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: InteractionId -> ()
NFData InteractionPoints
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: InteractionPoints -> ()
Eq InteractionId Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: InteractionId -> InteractionId -> Bool (/=) :: InteractionId -> InteractionId -> Bool
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
ToJSON InteractionId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: InteractionId -> Value # toEncoding :: InteractionId -> Encoding # toJSONList :: [InteractionId] -> Value # toEncodingList :: [InteractionId] -> Encoding # omitField :: InteractionId -> Bool #
type ConOfAbs InteractionId Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs InteractionId = Expr

data Modality Source #

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

Constructors

Modality

Fields

modRelevance :: Relevance
Legacy irrelevance. See Pfenning, LiCS 2001; Abel, Vezzosi and Winterhalter, 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

Instances details

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 #
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 #
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 #
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 #
Pretty Modality Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Modality -> Doc Source # prettyPrec :: Int -> Modality -> Doc Source # prettyList :: [Modality] -> Doc Source #
HasRange Modality Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Modality -> Range Source #
KillRange Modality Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Modality Source #
Verbalize Modality Source #
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Modality -> String Source #
PrettyTCM Modality Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Modality -> m Doc Source #
EmbPrj Modality Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Modality -> S Int32 Source # icod_ :: Modality -> S Int32 Source # value :: Int32 -> R Modality Source #
Unquote Modality Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Modality Source #
PartialOrd Modality Source #	Dominance ordering.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Modality Source #
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
Show Modality Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Modality -> ShowS show :: Modality -> String showList :: [Modality] -> ShowS
NFData Modality Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Modality -> ()
Eq Modality Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Modality -> Modality -> Bool (/=) :: Modality -> Modality -> Bool
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
IsVarSet () AllowedVar Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar Source #
LeftClosedPOMonoid (UnderComposition Modality) Source #
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality Source #
POMonoid (UnderAddition Modality) Source #
Instance details Defined in Agda.Syntax.Common
POMonoid (UnderComposition Modality) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderAddition Modality) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderComposition Modality) Source #
Instance details Defined in Agda.Syntax.Common
Monoid (UnderAddition Modality) Source #	Pointwise additive unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Modality mappend :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality mconcat :: [UnderAddition Modality] -> UnderAddition Modality
Monoid (UnderComposition Modality) Source #	Pointwise composition unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderComposition Modality mappend :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality mconcat :: [UnderComposition Modality] -> UnderComposition Modality
Semigroup (UnderAddition Modality) Source #	Pointwise addition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality # sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality
Semigroup (UnderComposition Modality) Source #	Pointwise composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality # sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality
type Rep Modality Source #
Instance details Defined in Agda.Syntax.Common type Rep Modality = D1 ('MetaData "Modality" "Agda.Syntax.Common" "Agda-2.6.4-inplace" '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))))

newtype ProblemId Source #

A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.

Constructors

ProblemId Nat

Instances

Instances details

EncodeTCM ProblemId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: ProblemId -> TCM Value Source #
Pretty ProblemId Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: ProblemId -> Doc Source # prettyPrec :: Int -> ProblemId -> Doc Source # prettyList :: [ProblemId] -> Doc Source #
HasFresh ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' TCState ProblemId Source # nextFresh' :: ProblemId -> ProblemId Source #
PrettyTCM ProblemId Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ProblemId -> m Doc Source #
Enum ProblemId Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: ProblemId -> ProblemId pred :: ProblemId -> ProblemId toEnum :: Int -> ProblemId fromEnum :: ProblemId -> Int enumFrom :: ProblemId -> [ProblemId] enumFromThen :: ProblemId -> ProblemId -> [ProblemId] enumFromTo :: ProblemId -> ProblemId -> [ProblemId] enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId]
Num ProblemId Source #
Instance details Defined in Agda.Syntax.Common Methods (+) :: ProblemId -> ProblemId -> ProblemId (-) :: ProblemId -> ProblemId -> ProblemId (*) :: ProblemId -> ProblemId -> ProblemId negate :: ProblemId -> ProblemId abs :: ProblemId -> ProblemId signum :: ProblemId -> ProblemId fromInteger :: Integer -> ProblemId
Integral ProblemId Source #
Instance details Defined in Agda.Syntax.Common Methods quot :: ProblemId -> ProblemId -> ProblemId rem :: ProblemId -> ProblemId -> ProblemId div :: ProblemId -> ProblemId -> ProblemId mod :: ProblemId -> ProblemId -> ProblemId quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId) divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId) toInteger :: ProblemId -> Integer
Real ProblemId Source #
Instance details Defined in Agda.Syntax.Common Methods toRational :: ProblemId -> Rational
Show ProblemId Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ProblemId -> ShowS show :: ProblemId -> String showList :: [ProblemId] -> ShowS
NFData ProblemId Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: ProblemId -> ()
Eq ProblemId Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: ProblemId -> ProblemId -> Bool (/=) :: ProblemId -> ProblemId -> Bool
Ord ProblemId Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: ProblemId -> ProblemId -> Ordering (<) :: ProblemId -> ProblemId -> Bool (<=) :: ProblemId -> ProblemId -> Bool (>) :: ProblemId -> ProblemId -> Bool (>=) :: ProblemId -> ProblemId -> Bool max :: ProblemId -> ProblemId -> ProblemId min :: ProblemId -> ProblemId -> ProblemId
ToJSON ProblemId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: ProblemId -> Value # toEncoding :: ProblemId -> Encoding # toJSONList :: [ProblemId] -> Value # toEncodingList :: [ProblemId] -> Encoding # omitField :: ProblemId -> Bool #
Monad m => MonadFresh ProblemId (PureConversionT m) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m ProblemId Source #

data Fixity Source #

Fixity of operators.

Constructors

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

Instances

Instances details

LensFixity Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods lensFixity :: Lens' Fixity Fixity 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 #
HasRange Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Fixity -> Range Source #
KillRange Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Fixity Source #
ToTerm Fixity Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity -> Term) Source # toTermR :: TCM (Fixity -> ReduceM Term) 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 #
Null Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Fixity Source # null :: Fixity -> Bool Source #
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 -> ()
Eq Fixity Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Fixity -> Fixity -> Bool (/=) :: Fixity -> Fixity -> Bool
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

data MetaId Source #

Meta-variable identifiers use the same structure as NameIds.

Constructors

MetaId
Fields metaId :: !Word64 metaModule :: !ModuleNameHash

Instances

Instances details

EncodeTCM MetaId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: MetaId -> TCM Value Source #
Pretty MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: MetaId -> Doc Source # prettyPrec :: Int -> MetaId -> Doc Source # prettyList :: [MetaId] -> Doc Source #
GetDefs MetaId Source #
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => MetaId -> m () Source #
NamesIn MetaId Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> MetaId -> m Source #
Reify MetaId Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo MetaId Source # Methods reify :: MonadReify m => MetaId -> m (ReifiesTo MetaId) Source # reifyWhen :: MonadReify m => Bool -> MetaId -> m (ReifiesTo MetaId) Source #
HasFresh MetaId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' TCState MetaId Source # nextFresh' :: MetaId -> MetaId Source #
IsInstantiatedMeta MetaId Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source #
UnFreezeMeta MetaId Source #
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #
PrettyTCM MetaId Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => MetaId -> m Doc Source #
FromTerm MetaId Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction MetaId) Source #
PrimTerm MetaId Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: MetaId -> TCM Term Source #
PrimType MetaId Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primType :: MetaId -> TCM Type Source #
ToTerm MetaId Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (MetaId -> Term) Source # toTermR :: TCM (MetaId -> ReduceM Term) 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 #
Unquote MetaId Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM MetaId Source #
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]
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
Show MetaId Source #	The record selectors are not included in the resulting strings.
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> MetaId -> ShowS show :: MetaId -> String showList :: [MetaId] -> ShowS
NFData MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: MetaId -> ()
Eq MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: MetaId -> MetaId -> Bool (/=) :: MetaId -> MetaId -> Bool
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
Hashable MetaId Source #
Instance details Defined in Agda.Syntax.Common Methods hashWithSalt :: Int -> MetaId -> Int hash :: MetaId -> Int
ToJSON MetaId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: MetaId -> Value # toEncoding :: MetaId -> Encoding # toJSONList :: [MetaId] -> Value # toEncodingList :: [MetaId] -> Encoding # omitField :: MetaId -> Bool #
Singleton MetaId MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: MetaId -> MetaSet Source #
Singleton MetaId () Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: MetaId -> () Source #
InstantiateFull (Judgement MetaId) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Judgement MetaId -> ReduceM (Judgement MetaId) Source #
type ReifiesTo MetaId Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo MetaId = Expr
type Rep MetaId Source #
Instance details Defined in Agda.Syntax.Common type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Just "metaModule") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash)))

data Ranged a Source #

Thing with range info.

Constructors

Ranged
Fields rangeOf :: Range rangedThing :: a

Instances

Instances details

MapNamedArgPattern NAP Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
Decoration Ranged Source #
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> Ranged a -> m (Ranged b) Source # distributeF :: Functor m => Ranged (m a) -> m (Ranged a) Source #
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 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)
Functor Ranged Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> Ranged a -> Ranged b (<$) :: a -> Ranged b -> Ranged a #
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 #
ExprLike a => ExprLike (Ranged a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Ranged a) Source # foldExpr :: FoldExprFn m (Ranged a) Source # traverseExpr :: TraverseExprFn m (Ranged a) Source # mapExpr :: (Expr -> Expr) -> Ranged a -> Ranged 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 #
Pretty a => Pretty (Ranged a) Source #	Ignores range.
Instance details Defined in Agda.Syntax.Common Methods pretty :: Ranged a -> Doc Source # prettyPrec :: Int -> Ranged a -> Doc Source # prettyList :: [Ranged a] -> Doc Source #
ExprLike a => ExprLike (Ranged a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Ranged a -> Ranged a Source # foldExpr :: Monoid m => (Expr -> m) -> Ranged a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Ranged a -> m (Ranged a) Source #
IsNoName a => IsNoName (Ranged a) Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: Ranged a -> Bool Source #
PatternVars (NamedArg (Pattern' a)) Source #
Instance details Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (NamedArg (Pattern' a)) Source # Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source #
HasRange (Ranged a) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Ranged a -> Range Source #
KillRange (Ranged a) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Ranged a) Source #
ToConcrete a => ToConcrete (Ranged a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Ranged a) Source # Methods toConcrete :: Ranged a -> AbsToCon (ConOfAbs (Ranged a)) Source # bindToConcrete :: Ranged a -> (ConOfAbs (Ranged a) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract c => ToAbstract (Ranged c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Ranged c) Source # Methods toAbstract :: Ranged c -> ScopeM (AbsOfCon (Ranged c)) Source #
PrettyTCM (NamedArg Expr) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc Source #
PrettyTCM (NamedArg Term) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Term -> m Doc Source #
PrettyTCM (Named_ Term) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Named_ Term -> 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 #
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 #
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 #
DeBruijn a => DeBruijn (Named_ a) Source #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Named_ a Source # debruijnNamedVar :: String -> Int -> Named_ a Source # deBruijnView :: Named_ a -> Maybe Int Source #
IApplyVars p => IApplyVars (NamedArg p) Source #
Instance details Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source #
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 -> ()
Eq a => Eq (Ranged a) Source #	Ignores range.
Instance details Defined in Agda.Syntax.Common Methods (==) :: Ranged a -> Ranged a -> Bool (/=) :: Ranged a -> Ranged a -> Bool
Ord a => Ord (Ranged a) Source #	Ignores range.
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
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
AddContext (List1 (NamedArg Name), Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # contextSize :: (List1 (NamedArg Name), Type) -> Nat 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 #
type PatternVarOut (NamedArg (Pattern' a)) Source #
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (NamedArg (Pattern' a)) = a
type ConOfAbs (Ranged a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Ranged a) = Ranged (ConOfAbs a)
type AbsOfCon (Ranged c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Ranged c) = Ranged (AbsOfCon c)

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

Instances details

Functor TerminationCheck Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> TerminationCheck a -> TerminationCheck b (<$) :: a -> TerminationCheck b -> TerminationCheck a #
KillRange m => KillRange (TerminationCheck m) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (TerminationCheck m) Source #
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 -> ()
Eq m => Eq (TerminationCheck m) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: TerminationCheck m -> TerminationCheck m -> Bool (/=) :: TerminationCheck m -> TerminationCheck m -> Bool

type Notation = [NotationPart] Source #

Notation as provided by the syntax declaration.

data Lock Source #

Constructors

IsNotLock
IsLock LockOrigin	In the future there might be different kinds of them. For now we assume lock weakening.

Instances

Instances details

LensLock Lock Source #
Instance details Defined in Agda.Syntax.Common Methods getLock :: Lock -> Lock Source # setLock :: Lock -> Lock -> Lock Source # mapLock :: (Lock -> Lock) -> Lock -> Lock Source #
EmbPrj Lock Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Lock -> S Int32 Source # icod_ :: Lock -> S Int32 Source # value :: Int32 -> R Lock Source #
Generic Lock Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Lock :: Type -> Type Methods from :: Lock -> Rep Lock x to :: Rep Lock x -> Lock
Show Lock Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Lock -> ShowS show :: Lock -> String showList :: [Lock] -> ShowS
NFData Lock Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Lock -> ()
Eq Lock Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Lock -> Lock -> Bool (/=) :: Lock -> Lock -> Bool
Ord Lock Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Lock -> Lock -> Ordering (<) :: Lock -> Lock -> Bool (<=) :: Lock -> Lock -> Bool (>) :: Lock -> Lock -> Bool (>=) :: Lock -> Lock -> Bool max :: Lock -> Lock -> Lock min :: Lock -> Lock -> Lock
type Rep Lock Source #
Instance details Defined in Agda.Syntax.Common type Rep Lock = D1 ('MetaData "Lock" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "IsNotLock" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsLock" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LockOrigin)))

data Cubical Source #

Variants of Cubical Agda.

Constructors

CErased
CFull

Instances

Instances details

EmbPrj Cubical Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Cubical -> S Int32 Source # icod_ :: Cubical -> S Int32 Source # value :: Int32 -> R Cubical Source #
Generic Cubical Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Cubical :: Type -> Type Methods from :: Cubical -> Rep Cubical x to :: Rep Cubical x -> Cubical
Show Cubical Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Cubical -> ShowS show :: Cubical -> String showList :: [Cubical] -> ShowS
NFData Cubical Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Cubical -> ()
Eq Cubical Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Cubical -> Cubical -> Bool (/=) :: Cubical -> Cubical -> Bool
type Rep Cubical Source #
Instance details Defined in Agda.Syntax.Common type Rep Cubical = D1 ('MetaData "Cubical" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "CErased" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CFull" 'PrefixI 'False) (U1 :: Type -> Type))

type NamedArg a = Arg (Named_ a) Source #

Only Hidden arguments can have names.

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

Instances details

(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 #
(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: ImportedName' a b -> Range Source #
(KillRange a, KillRange b) => KillRange (ImportedName' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportedName' a b) 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 #
(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 -> ()
(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
(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

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

Instances details

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 #
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]
Generic ConOrigin Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep ConOrigin :: Type -> Type Methods from :: ConOrigin -> Rep ConOrigin x to :: Rep ConOrigin x -> ConOrigin
Show ConOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ConOrigin -> ShowS show :: ConOrigin -> String showList :: [ConOrigin] -> ShowS
NFData ConOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: ConOrigin -> ()
Eq ConOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: ConOrigin -> ConOrigin -> Bool (/=) :: ConOrigin -> ConOrigin -> Bool
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
type Rep ConOrigin Source #
Instance details Defined in Agda.Syntax.Common type Rep ConOrigin = D1 ('MetaData "ConOrigin" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) ((C1 ('MetaCons "ConOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ConORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOSplit" 'PrefixI 'False) (U1 :: Type -> Type)))

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

Instances details

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 #
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]
Generic ProjOrigin Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep ProjOrigin :: Type -> Type Methods from :: ProjOrigin -> Rep ProjOrigin x to :: Rep ProjOrigin x -> ProjOrigin
Show ProjOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> ProjOrigin -> ShowS show :: ProjOrigin -> String showList :: [ProjOrigin] -> ShowS
NFData ProjOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: ProjOrigin -> ()
Eq ProjOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: ProjOrigin -> ProjOrigin -> Bool (/=) :: ProjOrigin -> ProjOrigin -> Bool
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
type Rep ProjOrigin Source #
Instance details Defined in Agda.Syntax.Common type Rep ProjOrigin = D1 ('MetaData "ProjOrigin" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "ProjPrefix" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ProjPostfix" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProjSystem" 'PrefixI 'False) (U1 :: Type -> Type)))

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.

The above comment is probably obsolete, as we currently have erasure (at0, Quantity0) for that. What's described here is probably shape-irrelevance (..). If you enable --experimental-irrelevance, then the type of an irrelevant function is forced to be shape-irrelevant. See: - https://doi.org/10.2168/LMCS-8(1:29)2012 example 2.8 (Not enforcing shape-irrelevant codomains can break subject reduction!) - https://dl.acm.org/doi/10.1145/3110277 - https://doi.org/10.1145/3209108.3209119

Irrelevant

The argument is irrelevant at compile- and runtime.

Instances

Instances details

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 #
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 #
HasRange Relevance Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Relevance -> Range 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 #
Verbalize Relevance Source #
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Relevance -> String Source #
PrettyTCM Relevance Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Relevance -> m Doc 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 #
Unquote Relevance Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Relevance Source #
PartialOrd Relevance Source #	More relevant is smaller.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Relevance Source #
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]
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
Show Relevance Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Relevance -> ShowS show :: Relevance -> String showList :: [Relevance] -> ShowS
NFData Relevance Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Relevance -> ()
Eq Relevance Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Relevance -> Relevance -> Bool (/=) :: Relevance -> Relevance -> Bool
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
LeftClosedPOMonoid (UnderComposition Relevance) Source #
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance Source #
POMonoid (UnderAddition Relevance) Source #
Instance details Defined in Agda.Syntax.Common
POMonoid (UnderComposition Relevance) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderAddition Relevance) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderComposition Relevance) Source #
Instance details Defined in Agda.Syntax.Common
Monoid (UnderAddition Relevance) Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Relevance mappend :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance mconcat :: [UnderAddition Relevance] -> UnderAddition Relevance
Monoid (UnderComposition Relevance) Source #	`Relevant` is the unit under composition.
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderComposition Relevance mappend :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance mconcat :: [UnderComposition Relevance] -> UnderComposition Relevance
Semigroup (UnderAddition Relevance) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance # sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance
Semigroup (UnderComposition Relevance) Source #	`Relevance` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance # sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance
type Rep Relevance Source #
Instance details Defined in Agda.Syntax.Common type Rep Relevance = D1 ('MetaData "Relevance" "Agda.Syntax.Common" "Agda-2.6.4-inplace" '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)))

data NameId Source #

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

Constructors

NameId !Word64 !ModuleNameHash

Instances

Instances details

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' TCState NameId 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 #
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]
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
Show NameId Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> NameId -> ShowS show :: NameId -> String showList :: [NameId] -> ShowS
NFData NameId Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: NameId -> ()
Eq NameId Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: NameId -> NameId -> Bool (/=) :: NameId -> NameId -> Bool
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
Hashable NameId Source #
Instance details Defined in Agda.Syntax.Common Methods hashWithSalt :: Int -> NameId -> Int hash :: NameId -> Int
MonadFresh NameId AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods fresh :: AbsToCon 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.4-inplace" '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 ModuleNameHash)))

data WithHiding a Source #

Decorating something with Hiding information.

Constructors

WithHiding
Fields whHiding :: !Hiding whThing :: a

Instances

Instances details

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 #
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 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)
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
Functor WithHiding Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> WithHiding a -> WithHiding b (<$) :: a -> WithHiding b -> WithHiding a #
ExprLike a => ExprLike (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (WithHiding a) Source # foldExpr :: FoldExprFn m (WithHiding a) Source # traverseExpr :: TraverseExprFn m (WithHiding a) Source # mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a 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 #
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 #
ExprLike a => ExprLike (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a Source # foldExpr :: Monoid m => (Expr -> m) -> WithHiding a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WithHiding a -> m (WithHiding a) 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 #
HasRange a => HasRange (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: WithHiding a -> Range 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 #
ToConcrete a => ToConcrete (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (WithHiding a) Source # Methods toConcrete :: WithHiding a -> AbsToCon (ConOfAbs (WithHiding a)) Source # bindToConcrete :: WithHiding a -> (ConOfAbs (WithHiding a) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract c => ToAbstract (WithHiding c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (WithHiding c) Source # Methods toAbstract :: WithHiding c -> ScopeM (AbsOfCon (WithHiding c)) 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 #
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 #
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 #
Subst a => Subst (WithHiding a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg (WithHiding a) Source # Methods applySubst :: Substitution' (SubstArg (WithHiding a)) -> WithHiding a -> WithHiding a Source #
Show a => Show (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> WithHiding a -> ShowS 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 -> ()
Eq a => Eq (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: WithHiding a -> WithHiding a -> Bool (/=) :: WithHiding a -> WithHiding a -> Bool
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
AddContext (List1 (WithHiding Name), Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat 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 #
type ConOfAbs (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (WithHiding a) = WithHiding (ConOfAbs a)
type AbsOfCon (WithHiding c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (WithHiding c) = WithHiding (AbsOfCon c)
type SubstArg (WithHiding a) Source #
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (WithHiding a) = SubstArg a

data Associativity Source #

Associativity.

Constructors

NonAssoc
LeftAssoc
RightAssoc

Instances

Instances details

Pretty Associativity Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Associativity -> Doc Source # prettyPrec :: Int -> Associativity -> Doc Source # prettyList :: [Associativity] -> Doc Source #
ToTerm Associativity Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Associativity -> Term) Source # toTermR :: TCM (Associativity -> ReduceM Term) Source #
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 #
Show Associativity Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Associativity -> ShowS show :: Associativity -> String showList :: [Associativity] -> ShowS
Eq Associativity Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Associativity -> Associativity -> Bool (/=) :: Associativity -> Associativity -> Bool
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

newtype Constr a Source #

Constructors

Constr a

Instances

Instances details

ToConcrete (Constr Constructor) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Constr Constructor) Source # Methods toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor)) Source # bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon b Source #
type ConOfAbs (Constr Constructor) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Constr Constructor) = Declaration

data Overlappable Source #

Constructors

YesOverlap
NoOverlap

Instances

Instances details

Monoid Overlappable Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: Overlappable mappend :: Overlappable -> Overlappable -> Overlappable mconcat :: [Overlappable] -> Overlappable
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
Show Overlappable Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Overlappable -> ShowS show :: Overlappable -> String showList :: [Overlappable] -> ShowS
NFData Overlappable Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Overlappable -> ()
Eq Overlappable Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Overlappable -> Overlappable -> Bool (/=) :: Overlappable -> Overlappable -> Bool
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

type Arity = Nat Source #

data FileType Source #

Constructors

AgdaFileType
MdFileType
RstFileType
TexFileType
OrgFileType
TypstFileType

Instances

Instances details

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 #
Generic FileType Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep FileType :: Type -> Type Methods from :: FileType -> Rep FileType x to :: Rep FileType x -> FileType
Show FileType Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> FileType -> ShowS show :: FileType -> String showList :: [FileType] -> ShowS
NFData FileType Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: FileType -> ()
Eq FileType Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: FileType -> FileType -> Bool (/=) :: FileType -> FileType -> Bool
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
type Rep FileType Source #
Instance details Defined in Agda.Syntax.Common type Rep FileType = D1 ('MetaData "FileType" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) ((C1 ('MetaCons "AgdaFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MdFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RstFileType" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TexFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OrgFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypstFileType" 'PrefixI 'False) (U1 :: Type -> Type))))

data Language Source #

Agda variants.

Only some variants are tracked.

Constructors

WithoutK
WithK
Cubical Cubical

Instances

Instances details

KillRange Language Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Language Source #
EmbPrj Language Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Language -> S Int32 Source # icod_ :: Language -> S Int32 Source # value :: Int32 -> R Language Source #
Generic Language Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Language :: Type -> Type Methods from :: Language -> Rep Language x to :: Rep Language x -> Language
Show Language Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Language -> ShowS show :: Language -> String showList :: [Language] -> ShowS
NFData Language Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Language -> ()
Eq Language Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Language -> Language -> Bool (/=) :: Language -> Language -> Bool
type Rep Language Source #
Instance details Defined in Agda.Syntax.Common type Rep Language = D1 ('MetaData "Language" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "WithoutK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "WithK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cubical" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Cubical))))

data RecordDirectives' a Source #

Constructors

RecordDirectives
Fields recInductive :: Maybe (Ranged Induction) recHasEta :: Maybe HasEta0 recPattern :: Maybe Range recConstructor :: Maybe a

Instances

Instances details

DeclaredNames RecordDirectives Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RecordDirectives -> m Source #
Functor RecordDirectives' Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> RecordDirectives' a -> RecordDirectives' b (<$) :: a -> RecordDirectives' b -> RecordDirectives' a #
HasRange a => HasRange (RecordDirectives' a) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: RecordDirectives' a -> Range Source #
KillRange a => KillRange (RecordDirectives' a) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (RecordDirectives' a) Source #
Show a => Show (RecordDirectives' a) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> RecordDirectives' a -> ShowS show :: RecordDirectives' a -> String showList :: [RecordDirectives' a] -> ShowS
NFData a => NFData (RecordDirectives' a) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: RecordDirectives' a -> ()
Eq a => Eq (RecordDirectives' a) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: RecordDirectives' a -> RecordDirectives' a -> Bool (/=) :: RecordDirectives' a -> RecordDirectives' a -> Bool

type HasEta0 = HasEta' () Source #

data HasEta' a Source #

Does a record come with eta-equality?

Constructors

YesEta
NoEta a

Instances

Instances details

CopatternMatchingAllowed HasEta Source #
Instance details Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: HasEta -> Bool Source #
PatternMatchingAllowed HasEta Source #
Instance details Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source #
Foldable HasEta' Source #
Instance details Defined in Agda.Syntax.Common Methods fold :: Monoid m => HasEta' m -> m foldMap :: Monoid m => (a -> m) -> HasEta' a -> m foldMap' :: Monoid m => (a -> m) -> HasEta' a -> m foldr :: (a -> b -> b) -> b -> HasEta' a -> b foldr' :: (a -> b -> b) -> b -> HasEta' a -> b foldl :: (b -> a -> b) -> b -> HasEta' a -> b foldl' :: (b -> a -> b) -> b -> HasEta' a -> b foldr1 :: (a -> a -> a) -> HasEta' a -> a foldl1 :: (a -> a -> a) -> HasEta' a -> a toList :: HasEta' a -> [a] null :: HasEta' a -> Bool length :: HasEta' a -> Int elem :: Eq a => a -> HasEta' a -> Bool maximum :: Ord a => HasEta' a -> a minimum :: Ord a => HasEta' a -> a sum :: Num a => HasEta' a -> a product :: Num a => HasEta' a -> a
Traversable HasEta' Source #
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> HasEta' a -> f (HasEta' b) sequenceA :: Applicative f => HasEta' (f a) -> f (HasEta' a) mapM :: Monad m => (a -> m b) -> HasEta' a -> m (HasEta' b) sequence :: Monad m => HasEta' (m a) -> m (HasEta' a)
Functor HasEta' Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> HasEta' a -> HasEta' b (<$) :: a -> HasEta' b -> HasEta' a #
HasRange a => HasRange (HasEta' a) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: HasEta' a -> Range Source #
KillRange a => KillRange (HasEta' a) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (HasEta' a) Source #
EmbPrj a => EmbPrj (HasEta' a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: HasEta' a -> S Int32 Source # icod_ :: HasEta' a -> S Int32 Source # value :: Int32 -> R (HasEta' a) Source #
Show a => Show (HasEta' a) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> HasEta' a -> ShowS show :: HasEta' a -> String showList :: [HasEta' a] -> ShowS
NFData a => NFData (HasEta' a) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: HasEta' a -> ()
Eq a => Eq (HasEta' a) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: HasEta' a -> HasEta' a -> Bool (/=) :: HasEta' a -> HasEta' a -> Bool
Ord a => Ord (HasEta' a) Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: HasEta' a -> HasEta' a -> Ordering (<) :: HasEta' a -> HasEta' a -> Bool (<=) :: HasEta' a -> HasEta' a -> Bool (>) :: HasEta' a -> HasEta' a -> Bool (>=) :: HasEta' a -> HasEta' a -> Bool max :: HasEta' a -> HasEta' a -> HasEta' a min :: HasEta' a -> HasEta' a -> HasEta' a

type HasEta = HasEta' PatternOrCopattern Source #

Pattern and copattern matching is allowed in the presence of eta.

In the absence of eta, we have to choose whether we want to allow matching on the constructor or copattern matching with the projections. Having both leads to breakage of subject reduction (issue #4560).

data PatternOrCopattern Source #

For a record without eta, which type of matching do we allow?

Constructors

PatternMatching	Can match on the record constructor.
CopatternMatching	Can copattern match using the projections. (Default.)

Instances

Instances details

CopatternMatchingAllowed HasEta Source #
Instance details Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: HasEta -> Bool Source #
CopatternMatchingAllowed PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: PatternOrCopattern -> Bool Source #
PatternMatchingAllowed HasEta Source #
Instance details Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source #
PatternMatchingAllowed PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: PatternOrCopattern -> Bool Source #
HasRange PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: PatternOrCopattern -> Range Source #
KillRange PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT PatternOrCopattern Source #
EmbPrj PatternOrCopattern Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PatternOrCopattern -> S Int32 Source # icod_ :: PatternOrCopattern -> S Int32 Source # value :: Int32 -> R PatternOrCopattern Source #
Bounded PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods minBound :: PatternOrCopattern maxBound :: PatternOrCopattern
Enum PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: PatternOrCopattern -> PatternOrCopattern pred :: PatternOrCopattern -> PatternOrCopattern toEnum :: Int -> PatternOrCopattern fromEnum :: PatternOrCopattern -> Int enumFrom :: PatternOrCopattern -> [PatternOrCopattern] enumFromThen :: PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] enumFromTo :: PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] enumFromThenTo :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern]
Show PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> PatternOrCopattern -> ShowS show :: PatternOrCopattern -> String showList :: [PatternOrCopattern] -> ShowS
NFData PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: PatternOrCopattern -> ()
Eq PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: PatternOrCopattern -> PatternOrCopattern -> Bool (/=) :: PatternOrCopattern -> PatternOrCopattern -> Bool
Ord PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: PatternOrCopattern -> PatternOrCopattern -> Ordering (<) :: PatternOrCopattern -> PatternOrCopattern -> Bool (<=) :: PatternOrCopattern -> PatternOrCopattern -> Bool (>) :: PatternOrCopattern -> PatternOrCopattern -> Bool (>=) :: PatternOrCopattern -> PatternOrCopattern -> Bool max :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern min :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern

class PatternMatchingAllowed a where Source #

Can we pattern match on the record constructor?

Methods

patternMatchingAllowed :: a -> Bool Source #

Instances

Instances details

PatternMatchingAllowed HasEta Source #
Instance details Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source #
PatternMatchingAllowed PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: PatternOrCopattern -> Bool Source #
PatternMatchingAllowed Induction Source #
Instance details Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: Induction -> Bool Source #
PatternMatchingAllowed DataOrRecord Source #
Instance details Defined in Agda.Syntax.Internal Methods patternMatchingAllowed :: DataOrRecord -> Bool Source #
PatternMatchingAllowed EtaEquality Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods patternMatchingAllowed :: EtaEquality -> Bool Source #

class CopatternMatchingAllowed a where Source #

Can we construct a record by copattern matching?

Methods

copatternMatchingAllowed :: a -> Bool Source #

Instances

Instances details

CopatternMatchingAllowed HasEta Source #
Instance details Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: HasEta -> Bool Source #
CopatternMatchingAllowed PatternOrCopattern Source #
Instance details Defined in Agda.Syntax.Common Methods copatternMatchingAllowed :: PatternOrCopattern -> Bool Source #
CopatternMatchingAllowed ConHead Source #
Instance details Defined in Agda.Syntax.Internal Methods copatternMatchingAllowed :: ConHead -> Bool Source #
CopatternMatchingAllowed DataOrRecord Source #
Instance details Defined in Agda.Syntax.Internal Methods copatternMatchingAllowed :: DataOrRecord -> Bool Source #
CopatternMatchingAllowed EtaEquality Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods copatternMatchingAllowed :: EtaEquality -> Bool 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 #

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

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

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

default mapHiding :: LensArgInfo a => (Hiding -> Hiding) -> a -> a Source #

Instances

Instances details

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 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 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 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.Concrete Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding 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 a => LensHiding (Named nm a) Source #
Instance details Defined in Agda.Syntax.Common Methods getHiding :: Named nm a -> Hiding Source # setHiding :: Hiding -> Named nm a -> Named nm a Source # mapHiding :: (Hiding -> Hiding) -> Named nm a -> Named nm 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 #

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

Instances details

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 #

data Named name a Source #

Something potentially carrying a name.

Constructors

Named
Fields nameOf :: Maybe name namedThing :: a

Instances

Instances details

MapNamedArgPattern NAP Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP 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 #
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 #
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 #
PatternVars (NamedArg (Pattern' a)) Source #
Instance details Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (NamedArg (Pattern' a)) Source # Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source #
PrettyTCM (NamedArg Expr) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc Source #
PrettyTCM (NamedArg Term) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Term -> m Doc Source #
PrettyTCM (Named_ Term) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Named_ Term -> 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 #
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 #
DeBruijn a => DeBruijn (Named_ a) Source #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Named_ a Source # debruijnNamedVar :: String -> Int -> Named_ a Source # deBruijnView :: Named_ a -> Maybe Int Source #
IApplyVars p => IApplyVars (NamedArg p) Source #
Instance details Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source #
Decoration (Named name) Source #
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> Named name a -> m (Named name b) Source # distributeF :: Functor m => Named name (m a) -> m (Named name a) Source #
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 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)
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 #
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat 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 #
IsProjP a => IsProjP (Named n a) Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source #
APatternLike a => APatternLike (Named n a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (Named n a) Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (Named n a)) -> m -> m) -> Named n a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (Named n a)) -> m (Pattern' (ADotT (Named n a)))) -> (Pattern' (ADotT (Named n a)) -> m (Pattern' (ADotT (Named n a)))) -> Named n a -> m (Named n a) Source #
DeclaredNames a => DeclaredNames (Named name a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Named name a -> m Source #
ExprLike a => ExprLike (Named x a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Named x a) Source # foldExpr :: FoldExprFn m (Named x a) Source # traverseExpr :: TraverseExprFn m (Named x a) Source # mapExpr :: (Expr -> Expr) -> Named x a -> Named x a Source #
LensHiding a => LensHiding (Named nm a) Source #
Instance details Defined in Agda.Syntax.Common Methods getHiding :: Named nm a -> Hiding Source # setHiding :: Hiding -> Named nm a -> Named nm a Source # mapHiding :: (Hiding -> Hiding) -> Named nm a -> Named nm a Source #
LensNamed (Named name a) Source #
Instance details Defined in Agda.Syntax.Common Associated Types type NameOf (Named name a) Source # Methods lensNamed :: Lens' (Named name a) (Maybe (NameOf (Named name a))) 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 # foldExpr :: Monoid m => (Expr -> m) -> Named name a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Named name a -> m (Named name a) 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 #
NamesIn a => NamesIn (Named n a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Named n a -> m Source #
CountPatternVars a => CountPatternVars (Named x a) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Named x a -> Int Source #
PatternVarModalities a => PatternVarModalities (Named s a) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern Associated Types type PatVar (Named s a) Source # Methods patternVarModalities :: Named s a -> [(PatVar (Named s a), Modality)] Source #
HasRange a => HasRange (Named name a) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Named name a -> Range Source #
(KillRange name, KillRange a) => KillRange (Named name a) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Named name a) Source #
SetRange a => SetRange (Named name a) Source #
Instance details Defined in Agda.Syntax.Common Methods setRange :: Range -> Named name a -> Named name a Source #
ToConcrete a => ToConcrete (Named name a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Named name a) Source # Methods toConcrete :: Named name a -> AbsToCon (ConOfAbs (Named name a)) Source # bindToConcrete :: Named name a -> (ConOfAbs (Named name a) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract c => ToAbstract (Named name c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Named name c) Source # Methods toAbstract :: Named name c -> ScopeM (AbsOfCon (Named name c)) Source #
Reify i => Reify (Named n i) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (Named n i) Source # Methods reify :: MonadReify m => Named n i -> m (ReifiesTo (Named n i)) Source # reifyWhen :: MonadReify m => Bool -> Named n i -> m (ReifiesTo (Named n i)) Source #
ToAbstract r => ToAbstract (Named name r) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Named name r) Source # Methods toAbstract :: MonadReflectedToAbstract m => Named name r -> m (AbsOfRef (Named name r)) Source #
Free t => Free (Named nm t) Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Named nm t -> FreeM a c Source #
AddContext (List1 (NamedArg Name), Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # contextSize :: (List1 (NamedArg Name), Type) -> Nat 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 #
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)
IsFlexiblePattern a => IsFlexiblePattern (Named name a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Named name a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Named name a -> m Bool 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 #
Subst a => Subst (Named name a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg (Named name a) Source # Methods applySubst :: Substitution' (SubstArg (Named name a)) -> Named name a -> Named name a Source #
PiApplyM a => PiApplyM (Named n a) Source #
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Named n a -> m Type Source # piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Named n a -> m Type Source #
(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 -> ()
(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
(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
LabelPatVars a b => LabelPatVars (Named x a) (Named x b) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern Associated Types type PatVarLabel (Named x b) Source # Methods labelPatVars :: Named x a -> State [PatVarLabel (Named x b)] (Named x b) Source # unlabelPatVars :: Named x b -> Named x a 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 #
type PatternVarOut (NamedArg (Pattern' a)) Source #
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (NamedArg (Pattern' a)) = a
type ADotT (Named n a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern type ADotT (Named n a) = ADotT a
type NameOf (Named name a) Source #
Instance details Defined in Agda.Syntax.Common type NameOf (Named name a) = name
type PatVar (Named s a) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVar (Named s a) = PatVar a
type PatVarLabel (Named x b) Source #
Instance details Defined in Agda.Syntax.Internal.Pattern type PatVarLabel (Named x b) = PatVarLabel b
type ConOfAbs (Named name a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Named name a) = Named name (ConOfAbs a)
type AbsOfCon (Named name c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Named name c) = Named name (AbsOfCon c)
type ReifiesTo (Named n i) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Named n i) = Named n (ReifiesTo i)
type AbsOfRef (Named name r) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Named name r) = Named name (AbsOfRef r)
type SubstArg (Named name a) Source #
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Named name a) = SubstArg a

newtype UnderAddition t Source #

Type wrapper to indicate additive monoid/semigroup context.

Constructors

UnderAddition t

Instances

Instances details

Applicative UnderAddition Source #
Instance details Defined in Agda.Syntax.Common Methods pure :: a -> UnderAddition a (<>) :: UnderAddition (a -> b) -> UnderAddition a -> UnderAddition b # liftA2 :: (a -> b -> c) -> UnderAddition a -> UnderAddition b -> UnderAddition c (>) :: UnderAddition a -> UnderAddition b -> UnderAddition b (<*) :: UnderAddition a -> UnderAddition b -> UnderAddition a
Functor UnderAddition Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> UnderAddition a -> UnderAddition b (<$) :: a -> UnderAddition b -> UnderAddition a #
POMonoid (UnderAddition Cohesion) Source #
Instance details Defined in Agda.Syntax.Common
POMonoid (UnderAddition Modality) Source #
Instance details Defined in Agda.Syntax.Common
POMonoid (UnderAddition Quantity) Source #
Instance details Defined in Agda.Syntax.Common
POMonoid (UnderAddition Relevance) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderAddition Cohesion) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderAddition Modality) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderAddition Quantity) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderAddition Relevance) Source #
Instance details Defined in Agda.Syntax.Common
PartialOrd t => PartialOrd (UnderAddition t) Source #
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable (UnderAddition t) Source #
Monoid (UnderAddition Cohesion) Source #	`Squash` is the additive unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Cohesion mappend :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion mconcat :: [UnderAddition Cohesion] -> UnderAddition Cohesion
Monoid (UnderAddition Modality) Source #	Pointwise additive unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Modality mappend :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality mconcat :: [UnderAddition Modality] -> UnderAddition Modality
Monoid (UnderAddition Quantity) Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Quantity mappend :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity mconcat :: [UnderAddition Quantity] -> UnderAddition Quantity
Monoid (UnderAddition Relevance) Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Relevance mappend :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance mconcat :: [UnderAddition Relevance] -> UnderAddition Relevance
Semigroup (UnderAddition Cohesion) Source #	`Cohesion` forms a semigroup under addition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion # sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion
Semigroup (UnderAddition Modality) Source #	Pointwise addition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality # sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality
Semigroup (UnderAddition Quantity) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity # sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity
Semigroup (UnderAddition Relevance) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance # sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance
Show t => Show (UnderAddition t) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> UnderAddition t -> ShowS show :: UnderAddition t -> String showList :: [UnderAddition t] -> ShowS
Eq t => Eq (UnderAddition t) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: UnderAddition t -> UnderAddition t -> Bool (/=) :: UnderAddition t -> UnderAddition t -> Bool
Ord t => Ord (UnderAddition t) Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: UnderAddition t -> UnderAddition t -> Ordering (<) :: UnderAddition t -> UnderAddition t -> Bool (<=) :: UnderAddition t -> UnderAddition t -> Bool (>) :: UnderAddition t -> UnderAddition t -> Bool (>=) :: UnderAddition t -> UnderAddition t -> Bool max :: UnderAddition t -> UnderAddition t -> UnderAddition t min :: UnderAddition t -> UnderAddition t -> UnderAddition t

newtype UnderComposition t Source #

Type wrapper to indicate composition or multiplicative monoid/semigroup context.

Constructors

UnderComposition t

Instances

Instances details

Applicative UnderComposition Source #
Instance details Defined in Agda.Syntax.Common Methods pure :: a -> UnderComposition a (<>) :: UnderComposition (a -> b) -> UnderComposition a -> UnderComposition b # liftA2 :: (a -> b -> c) -> UnderComposition a -> UnderComposition b -> UnderComposition c (>) :: UnderComposition a -> UnderComposition b -> UnderComposition b (<*) :: UnderComposition a -> UnderComposition b -> UnderComposition a
Functor UnderComposition Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> UnderComposition a -> UnderComposition b (<$) :: a -> UnderComposition b -> UnderComposition a #
LeftClosedPOMonoid (UnderComposition Cohesion) Source #
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion Source #
LeftClosedPOMonoid (UnderComposition Modality) Source #
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality Source #
LeftClosedPOMonoid (UnderComposition Quantity) Source #
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity Source #
LeftClosedPOMonoid (UnderComposition Relevance) Source #
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance Source #
POMonoid (UnderComposition Cohesion) Source #
Instance details Defined in Agda.Syntax.Common
POMonoid (UnderComposition Modality) Source #
Instance details Defined in Agda.Syntax.Common
POMonoid (UnderComposition Quantity) Source #
Instance details Defined in Agda.Syntax.Common
POMonoid (UnderComposition Relevance) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderComposition Cohesion) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderComposition Modality) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderComposition Quantity) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderComposition Relevance) Source #
Instance details Defined in Agda.Syntax.Common
PartialOrd t => PartialOrd (UnderComposition t) Source #
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable (UnderComposition t) Source #
Monoid (UnderComposition Cohesion) Source #	`Continous` is the multiplicative unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderComposition Cohesion mappend :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion mconcat :: [UnderComposition Cohesion] -> UnderComposition Cohesion
Monoid (UnderComposition Modality) Source #	Pointwise composition unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderComposition Modality mappend :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality mconcat :: [UnderComposition Modality] -> UnderComposition Modality
Monoid (UnderComposition 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 :: UnderComposition Quantity mappend :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity mconcat :: [UnderComposition Quantity] -> UnderComposition Quantity
Monoid (UnderComposition Relevance) Source #	`Relevant` is the unit under composition.
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderComposition Relevance mappend :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance mconcat :: [UnderComposition Relevance] -> UnderComposition Relevance
Semigroup (UnderComposition Cohesion) Source #	`Cohesion` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion # sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion
Semigroup (UnderComposition Erased) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased
Semigroup (UnderComposition Modality) Source #	Pointwise composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality # sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality
Semigroup (UnderComposition Quantity) Source #	Composition of quantities (multiplication). `Quantity0` is dominant. `Quantity1` is neutral. Right-biased for origin.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity
Semigroup (UnderComposition Relevance) Source #	`Relevance` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance # sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance
Show t => Show (UnderComposition t) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> UnderComposition t -> ShowS show :: UnderComposition t -> String showList :: [UnderComposition t] -> ShowS
Eq t => Eq (UnderComposition t) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: UnderComposition t -> UnderComposition t -> Bool (/=) :: UnderComposition t -> UnderComposition t -> Bool
Ord t => Ord (UnderComposition t) Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: UnderComposition t -> UnderComposition t -> Ordering (<) :: UnderComposition t -> UnderComposition t -> Bool (<=) :: UnderComposition t -> UnderComposition t -> Bool (>) :: UnderComposition t -> UnderComposition t -> Bool (>=) :: UnderComposition t -> UnderComposition t -> Bool max :: UnderComposition t -> UnderComposition t -> UnderComposition t min :: UnderComposition t -> UnderComposition t -> UnderComposition t

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

Instances details

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 #
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 #
HasRange Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Quantity -> Range 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 #
Verbalize Quantity Source #
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Quantity -> String Source #
PrettyTCM Quantity Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Quantity -> m Doc 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 #
Unquote Quantity Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Quantity Source #
PartialOrd Quantity Source #	Note that the order is `ω ≤ 0,1`, more options is smaller.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Quantity Source #
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
Show Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Quantity -> ShowS show :: Quantity -> String showList :: [Quantity] -> ShowS
NFData Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Quantity -> ()
Eq Quantity Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Quantity -> Quantity -> Bool (/=) :: Quantity -> Quantity -> Bool
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
LeftClosedPOMonoid (UnderComposition Quantity) Source #
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity Source #
POMonoid (UnderAddition Quantity) Source #
Instance details Defined in Agda.Syntax.Common
POMonoid (UnderComposition Quantity) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderAddition Quantity) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderComposition Quantity) Source #
Instance details Defined in Agda.Syntax.Common
Monoid (UnderAddition Quantity) Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Quantity mappend :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity mconcat :: [UnderAddition Quantity] -> UnderAddition Quantity
Monoid (UnderComposition 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 :: UnderComposition Quantity mappend :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity mconcat :: [UnderComposition Quantity] -> UnderComposition Quantity
Semigroup (UnderAddition Quantity) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity # sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity
Semigroup (UnderComposition Quantity) Source #	Composition of quantities (multiplication). `Quantity0` is dominant. `Quantity1` is neutral. Right-biased for origin.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity
type Rep Quantity Source #
Instance details Defined in Agda.Syntax.Common type Rep Quantity = D1 ('MetaData "Quantity" "Agda.Syntax.Common" "Agda-2.6.4-inplace" '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))))

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

Instances details

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 #
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 #
HasRange Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Cohesion -> Range 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 #
Verbalize Cohesion Source #
Instance details Defined in Agda.TypeChecking.Errors Methods verbalize :: Cohesion -> String 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 #
PartialOrd Cohesion Source #	Flatter is smaller.
Instance details Defined in Agda.Syntax.Common Methods comparable :: Comparable Cohesion Source #
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]
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
Show Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Cohesion -> ShowS show :: Cohesion -> String showList :: [Cohesion] -> ShowS
NFData Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Cohesion -> ()
Eq Cohesion Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Cohesion -> Cohesion -> Bool (/=) :: Cohesion -> Cohesion -> Bool
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
LeftClosedPOMonoid (UnderComposition Cohesion) Source #
Instance details Defined in Agda.Syntax.Common Methods inverseCompose :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion Source #
POMonoid (UnderAddition Cohesion) Source #
Instance details Defined in Agda.Syntax.Common
POMonoid (UnderComposition Cohesion) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderAddition Cohesion) Source #
Instance details Defined in Agda.Syntax.Common
POSemigroup (UnderComposition Cohesion) Source #
Instance details Defined in Agda.Syntax.Common
Monoid (UnderAddition Cohesion) Source #	`Squash` is the additive unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderAddition Cohesion mappend :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion mconcat :: [UnderAddition Cohesion] -> UnderAddition Cohesion
Monoid (UnderComposition Cohesion) Source #	`Continous` is the multiplicative unit.
Instance details Defined in Agda.Syntax.Common Methods mempty :: UnderComposition Cohesion mappend :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion mconcat :: [UnderComposition Cohesion] -> UnderComposition Cohesion
Semigroup (UnderAddition Cohesion) Source #	`Cohesion` forms a semigroup under addition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion # sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion
Semigroup (UnderComposition Cohesion) Source #	`Cohesion` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion # sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion
type Rep Cohesion Source #
Instance details Defined in Agda.Syntax.Common type Rep Cohesion = D1 ('MetaData "Cohesion" "Agda.Syntax.Common" "Agda-2.6.4-inplace" '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)))

class LensModality a where Source #

Minimal complete definition

Nothing

Methods

getModality :: a -> Modality Source #

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

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

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

default mapModality :: LensArgInfo a => (Modality -> Modality) -> a -> a Source #

Instances

Instances details

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 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 MetaInfo Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getModality :: MetaInfo -> Modality Source # setModality :: Modality -> MetaInfo -> MetaInfo Source # mapModality :: (Modality -> Modality) -> MetaInfo -> MetaInfo Source #
LensModality MetaVariable Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getModality :: MetaVariable -> Modality Source # setModality :: Modality -> MetaVariable -> MetaVariable Source # mapModality :: (Modality -> Modality) -> MetaVariable -> MetaVariable Source #
LensModality RemoteMetaVariable Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getModality :: RemoteMetaVariable -> Modality Source # setModality :: Modality -> RemoteMetaVariable -> RemoteMetaVariable Source # mapModality :: (Modality -> Modality) -> RemoteMetaVariable -> RemoteMetaVariable 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 #

class LensRelevance a where Source #

A lens to access the Relevance attribute in data structures. Minimal implementation: getRelevance and mapRelevance or LensModality.

Minimal complete definition

Nothing

Methods

getRelevance :: a -> Relevance Source #

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

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

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

default mapRelevance :: LensModality a => (Relevance -> Relevance) -> a -> a Source #

Instances

Instances details

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 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 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 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 MetaInfo Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRelevance :: MetaInfo -> Relevance Source # setRelevance :: Relevance -> MetaInfo -> MetaInfo Source # mapRelevance :: (Relevance -> Relevance) -> MetaInfo -> MetaInfo Source #
LensRelevance MetaVariable Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRelevance :: MetaVariable -> Relevance Source # setRelevance :: Relevance -> MetaVariable -> MetaVariable Source # mapRelevance :: (Relevance -> Relevance) -> MetaVariable -> MetaVariable Source #
LensRelevance RemoteMetaVariable Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRelevance :: RemoteMetaVariable -> Relevance Source # setRelevance :: Relevance -> RemoteMetaVariable -> RemoteMetaVariable Source # mapRelevance :: (Relevance -> Relevance) -> RemoteMetaVariable -> RemoteMetaVariable 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 #

class LensQuantity a where Source #

Minimal complete definition

Nothing

Methods

getQuantity :: a -> Quantity Source #

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

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

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

default mapQuantity :: LensModality a => (Quantity -> Quantity) -> a -> a Source #

Instances

Instances details

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 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 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 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 MetaInfo Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getQuantity :: MetaInfo -> Quantity Source # setQuantity :: Quantity -> MetaInfo -> MetaInfo Source # mapQuantity :: (Quantity -> Quantity) -> MetaInfo -> MetaInfo Source #
LensQuantity MetaVariable Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getQuantity :: MetaVariable -> Quantity Source # setQuantity :: Quantity -> MetaVariable -> MetaVariable Source # mapQuantity :: (Quantity -> Quantity) -> MetaVariable -> MetaVariable Source #
LensQuantity RemoteMetaVariable Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getQuantity :: RemoteMetaVariable -> Quantity Source # setQuantity :: Quantity -> RemoteMetaVariable -> RemoteMetaVariable Source # mapQuantity :: (Quantity -> Quantity) -> RemoteMetaVariable -> RemoteMetaVariable 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 #

class LensCohesion a where Source #

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

Minimal complete definition

Nothing

Methods

getCohesion :: a -> Cohesion Source #

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

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

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

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

Instances

Instances details

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 #

data Q0Origin Source #

Origin of Quantity0.

Constructors

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

Instances

Instances details

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 #
HasRange Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Q0Origin -> Range 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 #
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 #
Null Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Q0Origin Source # null :: Q0Origin -> Bool Source #
Monoid Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: Q0Origin mappend :: Q0Origin -> Q0Origin -> Q0Origin mconcat :: [Q0Origin] -> 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
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
Show Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Q0Origin -> ShowS show :: Q0Origin -> String showList :: [Q0Origin] -> ShowS
NFData Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Q0Origin -> ()
Eq Q0Origin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Q0Origin -> Q0Origin -> Bool (/=) :: Q0Origin -> Q0Origin -> Bool
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
type Rep Q0Origin Source #
Instance details Defined in Agda.Syntax.Common type Rep Q0Origin = D1 ('MetaData "Q0Origin" "Agda.Syntax.Common" "Agda-2.6.4-inplace" '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

Instances details

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 #
HasRange Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Q1Origin -> Range 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 #
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 #
Null Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Q1Origin Source # null :: Q1Origin -> Bool Source #
Monoid Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: Q1Origin mappend :: Q1Origin -> Q1Origin -> Q1Origin mconcat :: [Q1Origin] -> 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
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
Show Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Q1Origin -> ShowS show :: Q1Origin -> String showList :: [Q1Origin] -> ShowS
NFData Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Q1Origin -> ()
Eq Q1Origin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Q1Origin -> Q1Origin -> Bool (/=) :: Q1Origin -> Q1Origin -> Bool
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
type Rep Q1Origin Source #
Instance details Defined in Agda.Syntax.Common type Rep Q1Origin = D1 ('MetaData "Q1Origin" "Agda.Syntax.Common" "Agda-2.6.4-inplace" '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

Instances details

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 #
HasRange QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: QωOrigin -> Range 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 #
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 #
Null QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: QωOrigin Source # null :: QωOrigin -> Bool Source #
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
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
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
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
NFData QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: QωOrigin -> ()
Eq QωOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: QωOrigin -> QωOrigin -> Bool (/=) :: QωOrigin -> QωOrigin -> Bool
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
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.4-inplace" '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))))

data Erased Source #

A special case of Quantity: erased or not.

Note that the Ord instance does *not* ignore the origin arguments.

Constructors

Erased Q0Origin
NotErased QωOrigin

Instances

Instances details

Pretty Erased Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Erased -> Doc Source # prettyPrec :: Int -> Erased -> Doc Source # prettyList :: [Erased] -> Doc Source #
HasRange Erased Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Erased -> Range Source #
KillRange Erased Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Erased Source #
PrettyTCM Erased Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Erased -> m Doc Source #
Generic Erased Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Erased :: Type -> Type Methods from :: Erased -> Rep Erased x to :: Rep Erased x -> Erased
Show Erased Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Erased -> ShowS show :: Erased -> String showList :: [Erased] -> ShowS
NFData Erased Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Erased -> ()
Eq Erased Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Erased -> Erased -> Bool (/=) :: Erased -> Erased -> Bool
Ord Erased Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Erased -> Erased -> Ordering (<) :: Erased -> Erased -> Bool (<=) :: Erased -> Erased -> Bool (>) :: Erased -> Erased -> Bool (>=) :: Erased -> Erased -> Bool max :: Erased -> Erased -> Erased min :: Erased -> Erased -> Erased
Semigroup (UnderComposition Erased) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased
type Rep Erased Source #
Instance details Defined in Agda.Syntax.Common type Rep Erased = D1 ('MetaData "Erased" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "Erased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Q0Origin)) :+: C1 ('MetaCons "NotErased" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QωOrigin)))

data Annotation Source #

We have a tuple of annotations, which might not be fully orthogonal.

Constructors

Annotation
Fields annLock :: Lock Fitch-style dependent right adjoints. See Modal Dependent Type Theory and Dependent Right Adjoints, arXiv:1804.05236.

Instances

Instances details

LensAnnotation Annotation Source #
Instance details Defined in Agda.Syntax.Common Methods getAnnotation :: Annotation -> Annotation Source # setAnnotation :: Annotation -> Annotation -> Annotation Source # mapAnnotation :: (Annotation -> Annotation) -> Annotation -> Annotation Source #
HasRange Annotation Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Annotation -> Range Source #
KillRange Annotation Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Annotation Source #
EmbPrj Annotation Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Annotation -> S Int32 Source # icod_ :: Annotation -> S Int32 Source # value :: Int32 -> R Annotation Source #
Generic Annotation Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep Annotation :: Type -> Type Methods from :: Annotation -> Rep Annotation x to :: Rep Annotation x -> Annotation
Show Annotation Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> Annotation -> ShowS show :: Annotation -> String showList :: [Annotation] -> ShowS
NFData Annotation Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Annotation -> ()
Eq Annotation Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Annotation -> Annotation -> Bool (/=) :: Annotation -> Annotation -> Bool
Ord Annotation Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: Annotation -> Annotation -> Ordering (<) :: Annotation -> Annotation -> Bool (<=) :: Annotation -> Annotation -> Bool (>) :: Annotation -> Annotation -> Bool (>=) :: Annotation -> Annotation -> Bool max :: Annotation -> Annotation -> Annotation min :: Annotation -> Annotation -> Annotation
type Rep Annotation Source #
Instance details Defined in Agda.Syntax.Common type Rep Annotation = D1 ('MetaData "Annotation" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "Annotation" 'PrefixI 'True) (S1 ('MetaSel ('Just "annLock") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lock)))

class LensAnnotation a where Source #

Minimal complete definition

Nothing

Methods

getAnnotation :: a -> Annotation Source #

default getAnnotation :: LensArgInfo a => a -> Annotation Source #

setAnnotation :: Annotation -> a -> a Source #

default setAnnotation :: LensArgInfo a => Annotation -> a -> a Source #

mapAnnotation :: (Annotation -> Annotation) -> a -> a Source #

Instances

Instances details

LensAnnotation Annotation Source #
Instance details Defined in Agda.Syntax.Common Methods getAnnotation :: Annotation -> Annotation Source # setAnnotation :: Annotation -> Annotation -> Annotation Source # mapAnnotation :: (Annotation -> Annotation) -> Annotation -> Annotation Source #
LensAnnotation ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods getAnnotation :: ArgInfo -> Annotation Source # setAnnotation :: Annotation -> ArgInfo -> ArgInfo Source # mapAnnotation :: (Annotation -> Annotation) -> ArgInfo -> ArgInfo Source #
LensAnnotation (Arg t) Source #
Instance details Defined in Agda.Syntax.Common Methods getAnnotation :: Arg t -> Annotation Source # setAnnotation :: Annotation -> Arg t -> Arg t Source # mapAnnotation :: (Annotation -> Annotation) -> Arg t -> Arg t Source #
LensAnnotation (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getAnnotation :: Dom' t e -> Annotation Source # setAnnotation :: Annotation -> Dom' t e -> Dom' t e Source # mapAnnotation :: (Annotation -> Annotation) -> Dom' t e -> Dom' t e Source #

data LockOrigin Source #

Constructors

LockOLock	The user wrote @lock.
LockOTick	The user wrote @tick.

Instances

Instances details

Bounded LockOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods minBound :: LockOrigin maxBound :: LockOrigin
Enum LockOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: LockOrigin -> LockOrigin pred :: LockOrigin -> LockOrigin toEnum :: Int -> LockOrigin fromEnum :: LockOrigin -> Int enumFrom :: LockOrigin -> [LockOrigin] enumFromThen :: LockOrigin -> LockOrigin -> [LockOrigin] enumFromTo :: LockOrigin -> LockOrigin -> [LockOrigin] enumFromThenTo :: LockOrigin -> LockOrigin -> LockOrigin -> [LockOrigin]
Generic LockOrigin Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep LockOrigin :: Type -> Type Methods from :: LockOrigin -> Rep LockOrigin x to :: Rep LockOrigin x -> LockOrigin
Show LockOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> LockOrigin -> ShowS show :: LockOrigin -> String showList :: [LockOrigin] -> ShowS
Eq LockOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: LockOrigin -> LockOrigin -> Bool (/=) :: LockOrigin -> LockOrigin -> Bool
Ord LockOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: LockOrigin -> LockOrigin -> Ordering (<) :: LockOrigin -> LockOrigin -> Bool (<=) :: LockOrigin -> LockOrigin -> Bool (>) :: LockOrigin -> LockOrigin -> Bool (>=) :: LockOrigin -> LockOrigin -> Bool max :: LockOrigin -> LockOrigin -> LockOrigin min :: LockOrigin -> LockOrigin -> LockOrigin
type Rep LockOrigin Source #
Instance details Defined in Agda.Syntax.Common type Rep LockOrigin = D1 ('MetaData "LockOrigin" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "LockOLock" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LockOTick" 'PrefixI 'False) (U1 :: Type -> Type))

class LensLock a where Source #

Minimal complete definition

getLock

Methods

getLock :: a -> Lock Source #

setLock :: Lock -> a -> a Source #

mapLock :: (Lock -> Lock) -> a -> a Source #

Instances

Instances details

LensLock ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods getLock :: ArgInfo -> Lock Source # setLock :: Lock -> ArgInfo -> ArgInfo Source # mapLock :: (Lock -> Lock) -> ArgInfo -> ArgInfo Source #
LensLock Lock Source #
Instance details Defined in Agda.Syntax.Common Methods getLock :: Lock -> Lock Source # setLock :: Lock -> Lock -> Lock Source # mapLock :: (Lock -> Lock) -> Lock -> Lock Source #
LensLock (Arg t) Source #
Instance details Defined in Agda.Syntax.Common Methods getLock :: Arg t -> Lock Source # setLock :: Lock -> Arg t -> Arg t Source # mapLock :: (Lock -> Lock) -> Arg t -> Arg t Source #
LensLock (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Methods getLock :: Dom' t e -> Lock Source # setLock :: Lock -> Dom' t e -> Dom' t e Source # mapLock :: (Lock -> Lock) -> Dom' t e -> Dom' t e Source #

data ArgInfo Source #

A function argument can be hidden and/or irrelevant.

Constructors

ArgInfo
Fields argInfoHiding :: Hiding argInfoModality :: Modality argInfoOrigin :: Origin argInfoFreeVariables :: FreeVariables argInfoAnnotation :: Annotation Sometimes we want a different kind of binder/pi-type, without it supporting any of the `Modality` interface.

Instances

Instances details

LensAnnotation ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods getAnnotation :: ArgInfo -> Annotation Source # setAnnotation :: Annotation -> ArgInfo -> ArgInfo Source # mapAnnotation :: (Annotation -> Annotation) -> ArgInfo -> 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 #
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 #
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 #
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 #
LensLock ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods getLock :: ArgInfo -> Lock Source # setLock :: Lock -> ArgInfo -> ArgInfo Source # mapLock :: (Lock -> Lock) -> 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 #
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 #
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 #
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 #
HasRange ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: ArgInfo -> Range Source #
KillRange ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT ArgInfo Source #
EqualSy ArgInfo Source #	Ignore origin and free variables.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: ArgInfo -> ArgInfo -> Bool Source #
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 #
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)
Unquote ArgInfo Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM ArgInfo Source #
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 -> ()
Eq ArgInfo Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: ArgInfo -> ArgInfo -> Bool (/=) :: ArgInfo -> ArgInfo -> Bool
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

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"
ExpandedPun	An expanded hidden argument pun.
Generalization	Inserted by the generalization process

Instances

Instances details

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 #
HasRange Origin Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Origin -> Range Source #
KillRange Origin Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Origin Source #
ChooseFlex Origin Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Origin -> Origin -> FlexChoice 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 #
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 -> ()
Eq Origin Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Origin -> Origin -> Bool (/=) :: Origin -> Origin -> Bool
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

data WithOrigin a Source #

Decorating something with Origin information.

Constructors

WithOrigin
Fields woOrigin :: !Origin woThing :: a

Instances

Instances details

MapNamedArgPattern NAP Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
Decoration WithOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) Source # distributeF :: Functor m => WithOrigin (m a) -> m (WithOrigin a) Source #
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 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)
Functor WithOrigin Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> WithOrigin a -> WithOrigin b (<$) :: a -> WithOrigin b -> WithOrigin a #
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 #
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 #
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 #
IsNoName a => IsNoName (WithOrigin a) Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods isNoName :: WithOrigin a -> Bool Source #
PatternVars (NamedArg (Pattern' a)) Source #
Instance details Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (NamedArg (Pattern' a)) Source # Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source #
HasRange a => HasRange (WithOrigin a) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: WithOrigin a -> Range 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 #
PrettyTCM (NamedArg Expr) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc Source #
PrettyTCM (NamedArg Term) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Term -> m Doc Source #
PrettyTCM (Named_ Term) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Named_ Term -> 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 #
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 #
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 #
DeBruijn a => DeBruijn (Named_ a) Source #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Named_ a Source # debruijnNamedVar :: String -> Int -> Named_ a Source # deBruijnView :: Named_ a -> Maybe Int Source #
IApplyVars p => IApplyVars (NamedArg p) Source #
Instance details Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source #
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 -> ()
Eq a => Eq (WithOrigin a) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: WithOrigin a -> WithOrigin a -> Bool (/=) :: WithOrigin a -> WithOrigin a -> Bool
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
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Rewriting.Clause Methods toNLPat :: NamedArg DeBruijnPattern -> Elim' NLPat Source #
AddContext (List1 (NamedArg Name), Type) Source #
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # contextSize :: (List1 (NamedArg Name), Type) -> Nat 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 #
type PatternVarOut (NamedArg (Pattern' a)) Source #
Instance details Defined in Agda.Syntax.Internal type PatternVarOut (NamedArg (Pattern' a)) = a

class LensOrigin a where Source #

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

Minimal complete definition

Nothing

Methods

getOrigin :: a -> Origin Source #

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

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

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

default mapOrigin :: LensArgInfo a => (Origin -> Origin) -> a -> a Source #

Instances

Instances details

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

data FreeVariables Source #

Constructors

UnknownFVs
KnownFVs IntSet

Instances

Instances details

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 #
KillRange FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT 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 #
Monoid FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: FreeVariables mappend :: FreeVariables -> FreeVariables -> FreeVariables mconcat :: [FreeVariables] -> FreeVariables
Semigroup FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: FreeVariables -> FreeVariables -> FreeVariables # sconcat :: NonEmpty FreeVariables -> FreeVariables stimes :: Integral b => b -> FreeVariables -> FreeVariables
Show FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> FreeVariables -> ShowS show :: FreeVariables -> String showList :: [FreeVariables] -> ShowS
NFData FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: FreeVariables -> ()
Eq FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: FreeVariables -> FreeVariables -> Bool (/=) :: FreeVariables -> FreeVariables -> Bool
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

class LensFreeVariables a where Source #

A lens to access the FreeVariables attribute in data structures. Minimal implementation: getFreeVariables and mapFreeVariables or LensArgInfo.

Minimal complete definition

Nothing

Methods

getFreeVariables :: a -> FreeVariables Source #

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

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

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

default mapFreeVariables :: LensArgInfo a => (FreeVariables -> FreeVariables) -> a -> a Source #

Instances

Instances details

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 #

class Eq a => Underscore a where Source #

Minimal complete definition

underscore

Methods

underscore :: a Source #

isUnderscore :: a -> Bool Source #

Instances

Instances details

Underscore Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods underscore :: Expr Source # isUnderscore :: Expr -> Bool Source #
Underscore Doc Source #
Instance details Defined in Agda.Syntax.Common Methods underscore :: Doc Source # isUnderscore :: Doc -> Bool Source #
Underscore Name Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods underscore :: Name Source # isUnderscore :: Name -> Bool Source #
Underscore QName Source #
Instance details Defined in Agda.Syntax.Concrete.Name Methods underscore :: QName Source # isUnderscore :: QName -> Bool Source #
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 #

type Named_ = Named NamedName Source #

Standard naming.

type NamedName = WithOrigin (Ranged ArgName) Source #

Standard argument names.

type ArgName = String Source #

Names in binders and arguments.

class LensNamed a where Source #

Accessor/editor for the nameOf component.

Minimal complete definition

Nothing

Associated Types

type NameOf a Source #

The type of the name

Methods

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

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

Instances

Instances details

LensNamed a => LensNamed (Arg a) Source #
Instance details Defined in Agda.Syntax.Common Associated Types type NameOf (Arg a) Source # Methods lensNamed :: Lens' (Arg a) (Maybe (NameOf (Arg a))) Source #
LensNamed (Maybe a) Source #
Instance details Defined in Agda.Syntax.Common Associated Types type NameOf (Maybe a) Source # Methods lensNamed :: Lens' (Maybe a) (Maybe (NameOf (Maybe a))) Source #
LensNamed (Named name a) Source #
Instance details Defined in Agda.Syntax.Common Associated Types type NameOf (Named name a) Source # Methods lensNamed :: Lens' (Named name a) (Maybe (NameOf (Named name a))) Source #
LensNamed (Dom' t e) Source #
Instance details Defined in Agda.Syntax.Internal Associated Types type NameOf (Dom' t e) Source # Methods lensNamed :: Lens' (Dom' t e) (Maybe (NameOf (Dom' t e))) Source #

type RawName = String Source #

A RawName is some sort of string.

type RString = Ranged RawName Source #

String with range info.

data IsInfix Source #

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

Constructors

InfixDef
PrefixDef

Instances

Instances details

Show IsInfix Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsInfix -> ShowS show :: IsInfix -> String showList :: [IsInfix] -> ShowS
Eq IsInfix Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsInfix -> IsInfix -> Bool (/=) :: IsInfix -> IsInfix -> Bool
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

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

Instances details

Pretty Access Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: Access -> Doc Source # prettyPrec :: Int -> Access -> Doc Source # prettyList :: [Access] -> Doc Source #
HasRange Access Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Access -> Range Source #
KillRange Access Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Access 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 #
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 -> ()
Eq Access Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Access -> Access -> Bool (/=) :: Access -> Access -> Bool
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

data IsAbstract Source #

Abstract or concrete.

Constructors

AbstractDef
ConcreteDef

Instances

Instances details

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 #
KillRange IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsAbstract Source #
EmbPrj IsAbstract Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsAbstract -> S Int32 Source # icod_ :: IsAbstract -> S Int32 Source # value :: Int32 -> R IsAbstract Source #
Monoid IsAbstract Source #	Default is `ConcreteDef`.
Instance details Defined in Agda.Syntax.Common Methods mempty :: IsAbstract mappend :: IsAbstract -> IsAbstract -> IsAbstract mconcat :: [IsAbstract] -> IsAbstract
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
Generic IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep IsAbstract :: Type -> Type Methods from :: IsAbstract -> Rep IsAbstract x to :: Rep IsAbstract x -> IsAbstract
Show IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsAbstract -> ShowS show :: IsAbstract -> String showList :: [IsAbstract] -> ShowS
NFData IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: IsAbstract -> ()
Eq IsAbstract Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsAbstract -> IsAbstract -> Bool (/=) :: IsAbstract -> IsAbstract -> Bool
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
type Rep IsAbstract Source #
Instance details Defined in Agda.Syntax.Common type Rep IsAbstract = D1 ('MetaData "IsAbstract" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "AbstractDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConcreteDef" 'PrefixI 'False) (U1 :: Type -> Type))

class LensIsAbstract a where Source #

Methods

lensIsAbstract :: Lens' a IsAbstract Source #

Instances

Instances details

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

class AnyIsAbstract a where Source #

Is any element of a collection an AbstractDef.

Minimal complete definition

Nothing

Methods

anyIsAbstract :: a -> IsAbstract Source #

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

Instances

Instances details

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

data IsInstance Source #

Is this definition eligible for instance search?

Constructors

InstanceDef Range	Range of the `instance` keyword.
NotInstanceDef

Instances

Instances details

HasRange IsInstance Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: IsInstance -> Range Source #
KillRange IsInstance Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsInstance Source #
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 -> ()
Eq IsInstance Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsInstance -> IsInstance -> Bool (/=) :: IsInstance -> IsInstance -> Bool
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

data IsMacro Source #

Is this a macro definition?

Constructors

MacroDef
NotMacroDef

Instances

Instances details

HasRange IsMacro Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: IsMacro -> Range Source #
KillRange IsMacro Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsMacro Source #
Generic IsMacro Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep IsMacro :: Type -> Type Methods from :: IsMacro -> Rep IsMacro x to :: Rep IsMacro x -> IsMacro
Show IsMacro Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsMacro -> ShowS show :: IsMacro -> String showList :: [IsMacro] -> ShowS
NFData IsMacro Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: IsMacro -> ()
Eq IsMacro Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsMacro -> IsMacro -> Bool (/=) :: IsMacro -> IsMacro -> Bool
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
type Rep IsMacro Source #
Instance details Defined in Agda.Syntax.Common type Rep IsMacro = D1 ('MetaData "IsMacro" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "MacroDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotMacroDef" 'PrefixI 'False) (U1 :: Type -> Type))

data IsOpaque Source #

Opaque or transparent.

Constructors

OpaqueDef !OpaqueId	This definition is opaque, and it is guarded by the given opaque block.
TransparentDef

Instances

Instances details

AllAreOpaque IsOpaque Source #
Instance details Defined in Agda.Syntax.Common Methods jointOpacity :: IsOpaque -> JointOpacity Source #
LensIsOpaque IsOpaque Source #
Instance details Defined in Agda.Syntax.Common Methods lensIsOpaque :: Lens' IsOpaque IsOpaque Source #
KillRange IsOpaque Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT IsOpaque Source #
EmbPrj IsOpaque Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: IsOpaque -> S Int32 Source # icod_ :: IsOpaque -> S Int32 Source # value :: Int32 -> R IsOpaque Source #
Generic IsOpaque Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep IsOpaque :: Type -> Type Methods from :: IsOpaque -> Rep IsOpaque x to :: Rep IsOpaque x -> IsOpaque
Show IsOpaque Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsOpaque -> ShowS show :: IsOpaque -> String showList :: [IsOpaque] -> ShowS
NFData IsOpaque Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: IsOpaque -> ()
Eq IsOpaque Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsOpaque -> IsOpaque -> Bool (/=) :: IsOpaque -> IsOpaque -> Bool
Ord IsOpaque Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: IsOpaque -> IsOpaque -> Ordering (<) :: IsOpaque -> IsOpaque -> Bool (<=) :: IsOpaque -> IsOpaque -> Bool (>) :: IsOpaque -> IsOpaque -> Bool (>=) :: IsOpaque -> IsOpaque -> Bool max :: IsOpaque -> IsOpaque -> IsOpaque min :: IsOpaque -> IsOpaque -> IsOpaque
type Rep IsOpaque Source #
Instance details Defined in Agda.Syntax.Common type Rep IsOpaque = D1 ('MetaData "IsOpaque" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "OpaqueDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 OpaqueId)) :+: C1 ('MetaCons "TransparentDef" 'PrefixI 'False) (U1 :: Type -> Type))

data OpaqueId Source #

The unique identifier of an opaque block. Second argument is the top-level module identifier.

Constructors

OpaqueId !Word64 !ModuleNameHash

Instances

Instances details

Pretty OpaqueId Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: OpaqueId -> Doc Source # prettyPrec :: Int -> OpaqueId -> Doc Source # prettyList :: [OpaqueId] -> Doc Source #
KillRange OpaqueId Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT OpaqueId Source #
HasFresh OpaqueId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' TCState OpaqueId Source # nextFresh' :: OpaqueId -> OpaqueId Source #
EmbPrj OpaqueId Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: OpaqueId -> S Int32 Source # icod_ :: OpaqueId -> S Int32 Source # value :: Int32 -> R OpaqueId Source #
Enum OpaqueId Source #
Instance details Defined in Agda.Syntax.Common Methods succ :: OpaqueId -> OpaqueId pred :: OpaqueId -> OpaqueId toEnum :: Int -> OpaqueId fromEnum :: OpaqueId -> Int enumFrom :: OpaqueId -> [OpaqueId] enumFromThen :: OpaqueId -> OpaqueId -> [OpaqueId] enumFromTo :: OpaqueId -> OpaqueId -> [OpaqueId] enumFromThenTo :: OpaqueId -> OpaqueId -> OpaqueId -> [OpaqueId]
Generic OpaqueId Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep OpaqueId :: Type -> Type Methods from :: OpaqueId -> Rep OpaqueId x to :: Rep OpaqueId x -> OpaqueId
Show OpaqueId Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> OpaqueId -> ShowS show :: OpaqueId -> String showList :: [OpaqueId] -> ShowS
NFData OpaqueId Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: OpaqueId -> ()
Eq OpaqueId Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: OpaqueId -> OpaqueId -> Bool (/=) :: OpaqueId -> OpaqueId -> Bool
Ord OpaqueId Source #
Instance details Defined in Agda.Syntax.Common Methods compare :: OpaqueId -> OpaqueId -> Ordering (<) :: OpaqueId -> OpaqueId -> Bool (<=) :: OpaqueId -> OpaqueId -> Bool (>) :: OpaqueId -> OpaqueId -> Bool (>=) :: OpaqueId -> OpaqueId -> Bool max :: OpaqueId -> OpaqueId -> OpaqueId min :: OpaqueId -> OpaqueId -> OpaqueId
Hashable OpaqueId Source #
Instance details Defined in Agda.Syntax.Common Methods hashWithSalt :: Int -> OpaqueId -> Int hash :: OpaqueId -> Int
type Rep OpaqueId Source #
Instance details Defined in Agda.Syntax.Common type Rep OpaqueId = D1 ('MetaData "OpaqueId" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "OpaqueId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash)))

class LensIsOpaque a where Source #

Methods

lensIsOpaque :: Lens' a IsOpaque Source #

Instances

Instances details

LensIsOpaque IsOpaque Source #
Instance details Defined in Agda.Syntax.Common Methods lensIsOpaque :: Lens' IsOpaque IsOpaque Source #
LensIsOpaque (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods lensIsOpaque :: Lens' (DefInfo' t) IsOpaque Source #

data JointOpacity Source #

Monoid representing the combined opaque blocks of a Foldable containing possibly-opaque declarations.

Constructors

UniqueOpaque !OpaqueId	Every definition agrees on what opaque block they belong to.
DifferentOpaque !(HashSet OpaqueId)	More than one opaque block was found.
NoOpaque	Nothing here is opaque.

Instances

Instances details

Monoid JointOpacity Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: JointOpacity mappend :: JointOpacity -> JointOpacity -> JointOpacity mconcat :: [JointOpacity] -> JointOpacity
Semigroup JointOpacity Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: JointOpacity -> JointOpacity -> JointOpacity # sconcat :: NonEmpty JointOpacity -> JointOpacity stimes :: Integral b => b -> JointOpacity -> JointOpacity

class AllAreOpaque a where Source #

Minimal complete definition

Nothing

Methods

jointOpacity :: a -> JointOpacity Source #

default jointOpacity :: (Foldable t, AllAreOpaque b, t b ~ a) => a -> JointOpacity Source #

Instances

Instances details

AllAreOpaque IsOpaque Source #
Instance details Defined in Agda.Syntax.Common Methods jointOpacity :: IsOpaque -> JointOpacity Source #
AllAreOpaque (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods jointOpacity :: DefInfo' t -> JointOpacity Source #
AllAreOpaque a => AllAreOpaque (Maybe a) Source #
Instance details Defined in Agda.Syntax.Common Methods jointOpacity :: Maybe a -> JointOpacity Source #
AllAreOpaque a => AllAreOpaque [a] Source #
Instance details Defined in Agda.Syntax.Common Methods jointOpacity :: [a] -> JointOpacity Source #

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

Instances details

Show PositionInName Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> PositionInName -> ShowS show :: PositionInName -> String showList :: [PositionInName] -> ShowS
Eq PositionInName Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: PositionInName -> PositionInName -> Bool (/=) :: PositionInName -> PositionInName -> Bool
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

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

Instances details

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 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)
Functor MaybePlaceholder Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b (<$) :: a -> MaybePlaceholder b -> 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 #
ExprLike a => ExprLike (MaybePlaceholder a) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> MaybePlaceholder a -> MaybePlaceholder a Source # foldExpr :: Monoid m => (Expr -> m) -> MaybePlaceholder a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> MaybePlaceholder a -> m (MaybePlaceholder a) Source #
HasRange a => HasRange (MaybePlaceholder a) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: MaybePlaceholder a -> Range Source #
KillRange a => KillRange (MaybePlaceholder a) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (MaybePlaceholder a) Source #
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 -> ()
Eq e => Eq (MaybePlaceholder e) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool (/=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool
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

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

Instances details

Pretty FixityLevel Source #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: FixityLevel -> Doc Source # prettyPrec :: Int -> FixityLevel -> Doc Source # prettyList :: [FixityLevel] -> Doc Source #
ToTerm FixityLevel Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (FixityLevel -> Term) Source # toTermR :: TCM (FixityLevel -> ReduceM Term) 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 #
Null FixityLevel Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: FixityLevel Source # null :: FixityLevel -> Bool Source #
Show FixityLevel Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> FixityLevel -> ShowS show :: FixityLevel -> String showList :: [FixityLevel] -> ShowS
NFData FixityLevel Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: FixityLevel -> ()
Eq FixityLevel Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: FixityLevel -> FixityLevel -> Bool (/=) :: FixityLevel -> FixityLevel -> Bool
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

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

Instances details

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 #
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 #
PrimTerm Fixity' Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Fixity' -> TCM Term Source #
PrimType Fixity' Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primType :: Fixity' -> TCM Type Source #
ToTerm Fixity' Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity' -> Term) Source # toTermR :: TCM (Fixity' -> ReduceM Term) 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 #
Null Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Fixity' Source # null :: Fixity' -> Bool Source #
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' -> ()
Eq Fixity' Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: Fixity' -> Fixity' -> Bool (/=) :: Fixity' -> Fixity' -> Bool

class LensFixity a where Source #

Methods

lensFixity :: Lens' a Fixity Source #

Instances

Instances details

LensFixity Name Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity :: Lens' Name Fixity Source #
LensFixity QName Source #
Instance details Defined in Agda.Syntax.Abstract.Name Methods lensFixity :: Lens' QName 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 #
LensFixity NewNotation Source #
Instance details Defined in Agda.Syntax.Notation Methods lensFixity :: Lens' NewNotation Fixity Source #
LensFixity AbstractName Source #
Instance details Defined in Agda.Syntax.Scope.Base Methods lensFixity :: Lens' AbstractName Fixity Source #
LensFixity (ThingWithFixity a) Source #
Instance details Defined in Agda.Syntax.Fixity Methods lensFixity :: Lens' (ThingWithFixity a) Fixity Source #

class LensFixity' a where Source #

Methods

lensFixity' :: Lens' a Fixity' Source #

Instances

Instances details

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

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 :: HidingDirective' n m impRenaming :: RenamingDirective' n m publicOpen :: Maybe Range Only for `open`. Exports the opened names from the current module.

Instances

Instances details

(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 #
(HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: ImportDirective' a b -> Range Source #
(KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (ImportDirective' a b) Source #
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 #
(HasRange n, HasRange m) => Monoid (ImportDirective' n m) Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: ImportDirective' n m mappend :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m mconcat :: [ImportDirective' n m] -> ImportDirective' n m
(HasRange n, HasRange m) => Semigroup (ImportDirective' n m) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m # sconcat :: NonEmpty (ImportDirective' n m) -> ImportDirective' n m stimes :: Integral b => b -> ImportDirective' n m -> ImportDirective' n m
(Show a, Show b) => Show (ImportDirective' a b)
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 -> ()
(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 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

Instances details

(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 #
(HasRange a, HasRange b) => HasRange (Using' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Using' a b -> Range Source #
(KillRange a, KillRange b) => KillRange (Using' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Using' a b) Source #
Null (Using' n m) Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: Using' n m Source # null :: Using' n m -> Bool Source #
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
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
(Show a, Show b) => Show (Using' a b)
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
(NFData a, NFData b) => NFData (Using' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: Using' a b -> ()
(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

type HidingDirective' n m = [ImportedName' n m] Source #

type RenamingDirective' n m = [Renaming' n m] 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

Instances details

(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 #
(HasRange a, HasRange b) => HasRange (Renaming' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Renaming' a b -> Range Source #
(KillRange a, KillRange b) => KillRange (Renaming' a b) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Renaming' a b) Source #
(Show a, Show b) => Show (Renaming' a b)
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 -> ()
(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 PositivityCheck Source #

Positivity check? (Default = True).

Constructors

YesPositivityCheck
NoPositivityCheck

Instances

Instances details

KillRange PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT PositivityCheck Source #
Monoid PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: PositivityCheck mappend :: PositivityCheck -> PositivityCheck -> PositivityCheck mconcat :: [PositivityCheck] -> PositivityCheck
Semigroup PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: PositivityCheck -> PositivityCheck -> PositivityCheck # sconcat :: NonEmpty PositivityCheck -> PositivityCheck stimes :: Integral b => b -> PositivityCheck -> PositivityCheck
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]
Generic PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep PositivityCheck :: Type -> Type Methods from :: PositivityCheck -> Rep PositivityCheck x to :: Rep PositivityCheck x -> PositivityCheck
Show PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> PositivityCheck -> ShowS show :: PositivityCheck -> String showList :: [PositivityCheck] -> ShowS
NFData PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: PositivityCheck -> ()
Eq PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: PositivityCheck -> PositivityCheck -> Bool (/=) :: PositivityCheck -> PositivityCheck -> Bool
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
type Rep PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common type Rep PositivityCheck = D1 ('MetaData "PositivityCheck" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "YesPositivityCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoPositivityCheck" 'PrefixI 'False) (U1 :: Type -> Type))

data UniverseCheck Source #

Universe check? (Default is yes).

Constructors

YesUniverseCheck
NoUniverseCheck

Instances

Instances details

KillRange UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT UniverseCheck Source #
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]
Generic UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep UniverseCheck :: Type -> Type Methods from :: UniverseCheck -> Rep UniverseCheck x to :: Rep UniverseCheck x -> UniverseCheck
Show UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> UniverseCheck -> ShowS show :: UniverseCheck -> String showList :: [UniverseCheck] -> ShowS
NFData UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: UniverseCheck -> ()
Eq UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: UniverseCheck -> UniverseCheck -> Bool (/=) :: UniverseCheck -> UniverseCheck -> Bool
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
type Rep UniverseCheck Source #
Instance details Defined in Agda.Syntax.Common type Rep UniverseCheck = D1 ('MetaData "UniverseCheck" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "YesUniverseCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoUniverseCheck" 'PrefixI 'False) (U1 :: Type -> Type))

data CoverageCheck Source #

Coverage check? (Default is yes).

Constructors

YesCoverageCheck
NoCoverageCheck

Instances

Instances details

KillRange CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT CoverageCheck Source #
Monoid CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: CoverageCheck mappend :: CoverageCheck -> CoverageCheck -> CoverageCheck mconcat :: [CoverageCheck] -> CoverageCheck
Semigroup CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck # sconcat :: NonEmpty CoverageCheck -> CoverageCheck stimes :: Integral b => b -> CoverageCheck -> CoverageCheck
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]
Generic CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Associated Types type Rep CoverageCheck :: Type -> Type Methods from :: CoverageCheck -> Rep CoverageCheck x to :: Rep CoverageCheck x -> CoverageCheck
Show CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> CoverageCheck -> ShowS show :: CoverageCheck -> String showList :: [CoverageCheck] -> ShowS
NFData CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: CoverageCheck -> ()
Eq CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: CoverageCheck -> CoverageCheck -> Bool (/=) :: CoverageCheck -> CoverageCheck -> Bool
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
type Rep CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common type Rep CoverageCheck = D1 ('MetaData "CoverageCheck" "Agda.Syntax.Common" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "YesCoverageCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoCoverageCheck" 'PrefixI 'False) (U1 :: Type -> Type))

data RewriteEqn' qn nm 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 nm is the type of names for pattern variables p is the type of patterns e is the type of expressions

Constructors

Rewrite (List1 (qn, e))	rewrite e
Invert qn (List1 (Named nm (p, e)))	with p <- e in eq

Instances

Instances details

ToAbstract RewriteEqn Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon RewriteEqn Source # Methods toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source #
Foldable (RewriteEqn' qn nm p) Source #
Instance details Defined in Agda.Syntax.Common Methods fold :: Monoid m => RewriteEqn' qn nm p m -> m foldMap :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m foldMap' :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m foldr :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b foldr' :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b foldl :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b foldl' :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b foldr1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a foldl1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a toList :: RewriteEqn' qn nm p a -> [a] null :: RewriteEqn' qn nm p a -> Bool length :: RewriteEqn' qn nm p a -> Int elem :: Eq a => a -> RewriteEqn' qn nm p a -> Bool maximum :: Ord a => RewriteEqn' qn nm p a -> a minimum :: Ord a => RewriteEqn' qn nm p a -> a sum :: Num a => RewriteEqn' qn nm p a -> a product :: Num a => RewriteEqn' qn nm p a -> a
Traversable (RewriteEqn' qn nm p) Source #
Instance details Defined in Agda.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> RewriteEqn' qn nm p a -> f (RewriteEqn' qn nm p b) sequenceA :: Applicative f => RewriteEqn' qn nm p (f a) -> f (RewriteEqn' qn nm p a) mapM :: Monad m => (a -> m b) -> RewriteEqn' qn nm p a -> m (RewriteEqn' qn nm p b) sequence :: Monad m => RewriteEqn' qn nm p (m a) -> m (RewriteEqn' qn nm p a)
Functor (RewriteEqn' qn nm p) Source #
Instance details Defined in Agda.Syntax.Common Methods fmap :: (a -> b) -> RewriteEqn' qn nm p a -> RewriteEqn' qn nm p b (<$) :: a -> RewriteEqn' qn nm p b -> RewriteEqn' qn nm p a #
(ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (RewriteEqn' qn nm p e) Source # foldExpr :: FoldExprFn m (RewriteEqn' qn nm p e) Source # traverseExpr :: TraverseExprFn m (RewriteEqn' qn nm p e) Source # mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e Source #
(Pretty nm, Pretty p, Pretty e) => Pretty (RewriteEqn' qn nm p e) Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: RewriteEqn' qn nm p e -> Doc Source # prettyPrec :: Int -> RewriteEqn' qn nm p e -> Doc Source # prettyList :: [RewriteEqn' qn nm p e] -> Doc Source #
(ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e Source # foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn nm p e -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e) Source #
(HasRange qn, HasRange nm, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e) Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: RewriteEqn' qn nm p e -> Range Source #
(KillRange qn, KillRange nm, KillRange e, KillRange p) => KillRange (RewriteEqn' qn nm p e) Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (RewriteEqn' qn nm p e) Source #
(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (RewriteEqn' qn BindName p a) Source # Methods toConcrete :: RewriteEqn' qn BindName p a -> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a)) Source # bindToConcrete :: RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #
(Show e, Show qn, Show nm, Show p) => Show (RewriteEqn' qn nm p e) Source #
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> RewriteEqn' qn nm p e -> ShowS show :: RewriteEqn' qn nm p e -> String showList :: [RewriteEqn' qn nm p e] -> ShowS
(NFData qn, NFData nm, NFData p, NFData e) => NFData (RewriteEqn' qn nm p e) Source #
Instance details Defined in Agda.Syntax.Common Methods rnf :: RewriteEqn' qn nm p e -> ()
(Eq e, Eq qn, Eq nm, Eq p) => Eq (RewriteEqn' qn nm p e) Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool (/=) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool
type AbsOfCon RewriteEqn Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr
type ConOfAbs (RewriteEqn' qn BindName p a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (RewriteEqn' qn BindName p a) = RewriteEqn' () Name (ConOfAbs p) (ConOfAbs a)
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

data ExpandedEllipsis Source #

Constructors

ExpandedEllipsis
Fields ellipsisRange :: Range ellipsisWithArgs :: Int
NoEllipsis

Instances

Instances details

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 #
Null ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods empty :: ExpandedEllipsis Source # null :: ExpandedEllipsis -> Bool Source #
Monoid ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods mempty :: ExpandedEllipsis mappend :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis mconcat :: [ExpandedEllipsis] -> ExpandedEllipsis
Semigroup ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis # sconcat :: NonEmpty ExpandedEllipsis -> ExpandedEllipsis stimes :: Integral b => b -> ExpandedEllipsis -> 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 -> ()
Eq ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods (==) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool (/=) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool

data NotationPart Source #

Notation parts.

Constructors

IdPart RString	An identifier part. For instance, for `_+_` the only identifier part is `+`.
HolePart Range (NamedArg (Ranged Int))	A hole: a place where argument expressions can be written. For instance, for `_+_` the two underscores are holes, and for `syntax Σ A (λ x → B) = B , A , x` the variables `A` and `B` are holes. The number is the position of the hole, counting from zero. For instance, the number for `A` is `0`, and the number for `B` is `1`.
VarPart Range (Ranged BoundVariablePosition)	A bound variable. The first range is the range of the variable in the right-hand side of the syntax declaration, and the second range is the range of the variable in the left-hand side.
WildPart (Ranged BoundVariablePosition)	A wildcard (an underscore in binding position).

Instances

Instances details

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

data BoundVariablePosition Source #

Positions of variables in syntax declarations.

Constructors

BoundVariablePosition

Fields

holeNumber :: !Int
The position (in the left-hand side of the syntax declaration) of the hole in which the variable is bound, counting from zero (and excluding parts that are not holes). For instance, for syntax Σ A (λ x → B) = B , A , x the number for x is 1, corresponding to B (0 would correspond to A).
varNumber :: !Int
The position in the list of variables for this particular variable, counting from zero, and including wildcards. For instance, for syntax F (λ x _ y → A) = y ! A ! x the number for x is 0, the number for _ is 1, and the number for y is 2.

Instances

Instances details

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

fromImportedName :: ImportedName' a a -> a Source #

partitionImportedNames :: [ImportedName' n m] -> ([n], [m]) Source #

Like partitionEithers.

defaultArgInfo :: ArgInfo Source #

defaultArg :: a -> Arg a Source #

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

Check for Quantity0.

defaultFixity :: Fixity Source #

isInstance :: LensHiding a => a -> Bool Source #

emptyRecordDirectives :: RecordDirectives' a Source #

hidingToString :: Hiding -> String 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 #

sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool Source #

Ignores Overlappable.

composeModality :: Modality -> Modality -> Modality Source #

Multiplicative monoid (standard monoid).

unitModality :: Modality Source #

Identity under composition

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).

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

Modality forms a pointwise additive monoid.

zeroModality :: Modality Source #

Identity under addition

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 #

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

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

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

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

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

usableCohesion 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.

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

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

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

Cohesion composition. Squash is dominant, Continuous is neutral.

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.

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).

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).

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.

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

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

Note that this function does not change quantities.

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

Combine inferred Relevance. The unit is Irrelevant.

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

Quantity forms an additive monoid with zero Quantity0.

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

Combine inferred Cohesion. The unit is Squash.

zeroRelevance :: Relevance Source #

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

zeroQuantity :: Quantity Source #

Identity element under addition

zeroCohesion :: Cohesion Source #

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

unitRelevance :: Relevance Source #

Identity element under composition

unitQuantity :: Quantity Source #

Identity element under composition

unitCohesion :: Cohesion Source #

Identity under composition

topModality :: Modality Source #

Absorptive element under addition.

topRelevance :: Relevance Source #

Absorptive element under addition.

topQuantity :: Quantity Source #

Absorptive element is ω.

topCohesion :: Cohesion Source #

Absorptive element under addition.

defaultModality :: Modality Source #

The default Modality Beware that this is neither the additive unit nor the unit under composition, because the default quantity is ω.

defaultRelevance :: Relevance Source #

Default Relevance is the identity element under composition

defaultQuantity :: Quantity Source #

Absorptive element! This differs from Relevance and Cohesion whose default is the multiplicative unit.

defaultCohesion :: Cohesion Source #

Default Cohesion is the identity element under composition

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

Equality ignoring origin.

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

Equality ignoring origin.

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

Equality ignoring origin.

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

Equality ignoring origin.

lModRelevance :: Lens' Modality Relevance Source #

lModQuantity :: Lens' Modality Quantity Source #

lModCohesion :: Lens' Modality Cohesion Source #

getRelevanceMod :: LensModality a => LensGet a Relevance Source #

setRelevanceMod :: LensModality a => LensSet a Relevance Source #

mapRelevanceMod :: LensModality a => LensMap a Relevance Source #

getQuantityMod :: LensModality a => LensGet a Quantity Source #

setQuantityMod :: LensModality a => LensSet a Quantity Source #

mapQuantityMod :: LensModality a => LensMap a Quantity Source #

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

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

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

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

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

applyQuantity :: LensQuantity a => Quantity -> a -> a Source #

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

inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a Source #

Left division by a Quantity. Used e.g. to modify context when going into a q argument.

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?

defaultErased :: Erased Source #

The default value of type Erased: not erased.

asQuantity :: Erased -> Quantity Source #

Erased can be embedded into Quantity.

erasedFromQuantity :: Quantity -> Maybe Erased Source #

Quantity can be projected onto Erased.

sameErased :: Erased -> Erased -> Bool Source #

Equality ignoring origin.

isErased :: Erased -> Bool Source #

Is the value "erased"?

composeErased :: Erased -> Erased -> Erased Source #

Composition of values of type Erased.

Erased is dominant. NotErased is neutral.

Right-biased for the origin.

allRelevances :: [Relevance] 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

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.

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

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

irrToNonStrict :: Relevance -> Relevance Source #

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

nonStrictToRel :: Relevance -> Relevance Source #

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

nonStrictToIrr :: Relevance -> Relevance Source #

defaultAnnotation :: Annotation Source #

defaultLock :: Lock Source #

allCohesions :: [Cohesion] Source #

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

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

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.

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

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

unknownFreeVariables :: FreeVariables Source #

noFreeVariables :: FreeVariables Source #

oneFreeVariable :: Int -> FreeVariables Source #

freeVariablesFromList :: [Int] -> FreeVariables Source #

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

getHidingArgInfo :: LensArgInfo a => LensGet a Hiding Source #

setHidingArgInfo :: LensArgInfo a => LensSet a Hiding Source #

mapHidingArgInfo :: LensArgInfo a => LensMap a Hiding Source #

getModalityArgInfo :: LensArgInfo a => LensGet a Modality Source #

setModalityArgInfo :: LensArgInfo a => LensSet a Modality Source #

mapModalityArgInfo :: LensArgInfo a => LensMap a Modality Source #

getOriginArgInfo :: LensArgInfo a => LensGet a Origin Source #

setOriginArgInfo :: LensArgInfo a => LensSet a Origin Source #

mapOriginArgInfo :: LensArgInfo a => LensMap a Origin Source #

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

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

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

isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool 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 #

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

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

unnamed :: a -> Named name a Source #

isUnnamed :: Named name a -> Maybe a Source #

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

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

getNameOf :: LensNamed a => a -> Maybe (NameOf a) Source #

setNameOf :: LensNamed a => Maybe (NameOf a) -> a -> a Source #

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

bareNameOf :: (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName Source #

bareNameWithDefault :: (LensNamed a, NameOf a ~ NamedName) => ArgName -> a -> ArgName Source #

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

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

fittingNamedArg :: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, 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@

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

argNameToString :: ArgName -> String Source #

stringToArgName :: String -> ArgName Source #

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

unranged :: a -> Ranged a Source #

Thing with no range info.

rawNameToString :: RawName -> String Source #

stringToRawName :: String -> RawName Source #

bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin Source #

Prefer user-written over system-inserted.

noPlaceholder :: e -> MaybePlaceholder e Source #

An abbreviation: noPlaceholder = NoPlaceholder Nothing.

noFixity :: Fixity Source #

noFixity' :: Fixity' Source #

noNotation :: Notation Source #

_fixityAssoc :: Lens' Fixity Associativity Source #

_fixityLevel :: Lens' Fixity FixityLevel 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.

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

setImportedName :: ImportedName' a a -> a -> ImportedName' a a Source #

module Agda.Syntax.TopLevelModuleName.Boot

data Induction Source #

Constructors

Inductive
CoInductive

Instances

Instances details

PatternMatchingAllowed Induction Source #
Instance details Defined in Agda.Syntax.Common Methods patternMatchingAllowed :: Induction -> Bool Source #
Pretty Induction Source #
Instance details Defined in Agda.Syntax.Common Methods pretty :: Induction -> Doc Source # prettyPrec :: Int -> Induction -> Doc Source # prettyList :: [Induction] -> Doc Source #
HasRange Induction Source #
Instance details Defined in Agda.Syntax.Common Methods getRange :: Induction -> Range Source #
KillRange Induction Source #
Instance details Defined in Agda.Syntax.Common Methods killRange :: KillRangeT Induction 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 #
Show Induction Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> Induction -> ShowS show :: Induction -> String showList :: [Induction] -> ShowS
NFData Induction Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods rnf :: Induction -> ()
Eq Induction Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: Induction -> Induction -> Bool (/=) :: Induction -> Induction -> Bool
Ord Induction Source #
Instance details Defined in Agda.Syntax.Common.Aspect 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

Orphan instances

Pretty Induction Source #
Instance details Methods pretty :: Induction -> Doc Source # prettyPrec :: Int -> Induction -> Doc Source # prettyList :: [Induction] -> Doc Source #
HasRange Induction Source #
Instance details Methods getRange :: Induction -> Range Source #
KillRange Induction Source #
Instance details Methods killRange :: KillRangeT Induction Source #