Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- type Type = Type' Term
- pattern Type :: Level' t -> Sort' t
- data Dom' t e = Dom {}
- telToList :: Tele (Dom t) -> [Dom (ArgName, t)]
- type Telescope = Tele (Dom Type)
- type Substitution = Substitution' Term
- type Dom = Dom' Term
- type Level = Level' Term
- data Term
- type Pattern = Pattern' PatVarName
- data Clause = Clause {
- clauseLHSRange :: Range
- clauseFullRange :: Range
- clauseTel :: Telescope
- namedClausePats :: NAPs
- clauseBody :: Maybe Term
- clauseType :: Maybe (Arg Type)
- clauseCatchall :: Bool
- clauseExact :: Maybe Bool
- clauseRecursive :: Maybe Bool
- clauseUnreachable :: Maybe Bool
- clauseEllipsis :: ExpandedEllipsis
- clauseWhereModule :: Maybe ModuleName
- type Elim = Elim' Term
- data Sort' t
- class PatternVars a where
- type PatternVarOut a
- patternVars :: a -> [Arg (Either (PatternVarOut a) Term)]
- type Sort = Sort' Term
- type DataOrRecord = DataOrRecord' PatternOrCopattern
- data Substitution' a
- = IdS
- | EmptyS Impossible
- | a :# (Substitution' a)
- | Strengthen Impossible !Int (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- type Args = [Arg Term]
- data Abs a
- class LensSort a where
- type Elims = [Elim]
- arity :: Type -> Nat
- data Level' t = Max !Integer [PlusLevel' t]
- data ConHead = ConHead {
- conName :: QName
- conDataRecord :: DataOrRecord
- conInductive :: Induction
- conFields :: [Arg QName]
- pattern Prop :: Level' t -> Sort' t
- pattern SSet :: Level' t -> Sort' t
- var :: Nat -> Term
- data PlusLevel' t = Plus !Integer t
- data Pattern' x
- = VarP PatternInfo x
- | DotP PatternInfo Term
- | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
- | LitP PatternInfo Literal
- | ProjP ProjOrigin QName
- | IApplyP PatternInfo Term Term x
- | DefP PatternInfo QName [NamedArg (Pattern' x)]
- class TermSize a where
- type Blocked = Blocked' Term
- type NotBlocked = NotBlocked' Term
- argFromDom :: Dom' t a -> Arg a
- namedArgFromDom :: Dom' t a -> NamedArg a
- domFromArg :: Arg a -> Dom a
- domFromNamedArg :: NamedArg a -> Dom a
- defaultDom :: a -> Dom a
- defaultArgDom :: ArgInfo -> a -> Dom a
- defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
- type NamedArgs = [NamedArg Term]
- data DataOrRecord' p
- class LensConName a where
- getConName :: a -> QName
- setConName :: QName -> a -> a
- mapConName :: (QName -> QName) -> a -> a
- type ConInfo = ConOrigin
- data Type'' t a = El {}
- type Type' a = Type'' Term a
- data Tele a
- data UnivSize
- isStrictDataSort :: Sort' t -> Bool
- type PlusLevel = PlusLevel' Term
- type LevelAtom = Term
- newtype BraveTerm = BraveTerm {}
- type Blocked_ = Blocked ()
- type NAPs = [NamedArg DeBruijnPattern]
- type DeBruijnPattern = Pattern' DBPatVar
- clausePats :: Clause -> [Arg DeBruijnPattern]
- type PatVarName = ArgName
- patVarNameToString :: PatVarName -> String
- nameToPatVarName :: Name -> PatVarName
- data PatternInfo = PatternInfo {
- patOrigin :: PatOrigin
- patAsNames :: [Name]
- data PatOrigin
- = PatOSystem
- | PatOSplit
- | PatOVar Name
- | PatODot
- | PatOWild
- | PatOCon
- | PatORec
- | PatOLit
- | PatOAbsurd
- defaultPatternInfo :: PatternInfo
- data ConPatternInfo = ConPatternInfo {
- conPInfo :: PatternInfo
- conPRecord :: Bool
- conPFallThrough :: Bool
- conPType :: Maybe (Arg Type)
- conPLazy :: Bool
- varP :: a -> Pattern' a
- dotP :: Term -> Pattern' a
- litP :: Literal -> Pattern' a
- data DBPatVar = DBPatVar {
- dbPatVarName :: PatVarName
- dbPatVarIndex :: !Int
- namedVarP :: PatVarName -> Named_ Pattern
- namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
- absurdP :: Int -> DeBruijnPattern
- absurdPatternName :: PatVarName
- noConPatternInfo :: ConPatternInfo
- toConPatternInfo :: ConInfo -> ConPatternInfo
- fromConPatternInfo :: ConPatternInfo -> ConInfo
- type family PatternVarOut a
- patternInfo :: Pattern' x -> Maybe PatternInfo
- patternOrigin :: Pattern' x -> Maybe PatOrigin
- properlyMatching :: Pattern' a -> Bool
- properlyMatching' :: Bool -> Bool -> Pattern' a -> Bool
- type PatternSubstitution = Substitution' DeBruijnPattern
- data EqualityView
- data EqualityTypeData = EqualityTypeData {}
- pattern EqualityType :: Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView
- eqtSort :: EqualityView -> Sort
- eqtName :: EqualityView -> QName
- eqtParams :: EqualityView -> Args
- eqtType :: EqualityView -> Arg Term
- eqtLhs :: EqualityView -> Arg Term
- eqtRhs :: EqualityView -> Arg Term
- isEqualityType :: EqualityView -> Bool
- data PathView
- isPathType :: PathView -> Bool
- data IntervalView
- isIOne :: IntervalView -> Bool
- absurdBody :: Abs Term
- isAbsurdBody :: Abs Term -> Bool
- isAbsurdPatternName :: PatVarName -> Bool
- dontCare :: Term -> Term
- type DummyTermKind = String
- dummyLocName :: CallStack -> String
- dummyTermWith :: DummyTermKind -> CallStack -> Term
- dummyLevel :: CallStack -> Level
- atomicLevel :: t -> Level' t
- dummyTerm :: CallStack -> Term
- __DUMMY_TERM__ :: HasCallStack => Term
- __DUMMY_LEVEL__ :: HasCallStack => Level
- dummySort :: CallStack -> Sort
- __DUMMY_SORT__ :: HasCallStack => Sort
- dummyType :: CallStack -> Type
- __DUMMY_TYPE__ :: HasCallStack => Type
- dummyDom :: CallStack -> Dom Type
- __DUMMY_DOM__ :: HasCallStack => Dom Type
- pattern ClosedLevel :: Integer -> Level
- varSort :: Int -> Sort
- tmSort :: Term -> Sort
- tmSSort :: Term -> Sort
- levelPlus :: Integer -> Level -> Level
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- mkProp :: Integer -> Sort
- mkSSet :: Integer -> Sort
- isSort :: Term -> Maybe Sort
- impossibleTerm :: CallStack -> Term
- mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
- mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
- replaceEmptyName :: ArgName -> Tele a -> Tele a
- type ListTel' a = [Dom (a, Type)]
- type ListTel = ListTel' ArgName
- telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
- telFromList :: ListTel -> Telescope
- listTel :: Lens' Telescope ListTel
- class TelToArgs a where
- class SgTel a where
- stripDontCare :: Term -> Term
- class Suggest a where
- suggestName :: a -> Maybe String
- data Suggestion = Suggest a => Suggestion a
- suggests :: [Suggestion] -> String
- unSpine :: Term -> Term
- unSpine' :: (ProjOrigin -> QName -> Bool) -> Term -> Term
- hasElims :: Term -> Maybe (Elims -> Term, Elims)
- type family TypeOf a
- pDom :: LensHiding a => a -> Doc -> Doc
- prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
- module Agda.Syntax.Internal.Blockers
- module Agda.Syntax.Internal.Elim
- module Agda.Syntax.Internal.Univ
- module Agda.Syntax.Abstract.Name
- data MetaId = MetaId {
- metaId :: !Word64
- metaModule :: !ModuleNameHash
- newtype ProblemId = ProblemId Nat
Documentation
Similar to Arg
, but we need to distinguish
an irrelevance annotation in a function domain
(the domain itself is not irrelevant!)
from an irrelevant argument.
Dom
is used in Pi
of internal syntax, in Context
and Telescope
.
Arg
is used for actual arguments (Var
, Con
, Def
etc.)
and in Abstract
syntax and other situations.
- cubical
- When
annFinite (argInfoAnnotation domInfo) = True
for the domain of aPi
type, the elements should be compared by tabulating the domain type. Only supported in case the domain type is primIsOne, to obtain the correct equality for partial elements.
Instances
type Substitution = Substitution' Term Source #
Raw values.
Def
is used for both defined and undefined constants.
Assume there is a type declaration and a definition for
every constant, even if the definition is an empty
list of clauses.
Var !Int Elims |
|
Lam ArgInfo (Abs Term) | Terms are beta normal. Relevance is ignored |
Lit Literal | |
Def QName Elims |
|
Con ConHead ConInfo Elims |
|
Pi (Dom Type) (Abs Type) | dependent or non-dependent function space |
Sort Sort | |
Level Level | |
MetaV !MetaId Elims | |
DontCare Term | Irrelevant stuff in relevant position, but created
in an irrelevant context. Basically, an internal
version of the irrelevance axiom |
Dummy String Elims | A (part of a) term or type which is only used for internal purposes.
Replaces the |
Instances
Pretty Level Source # | |||||
Pretty PlusLevel Source # | |||||
Pretty Sort Source # | |||||
Pretty Term Source # | |||||
Pretty Type Source # | |||||
Pretty CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.CompiledClause pretty :: CompiledClauses -> Doc Source # prettyPrec :: Int -> CompiledClauses -> Doc Source # prettyList :: [CompiledClauses] -> Doc Source # | |||||
LensSort Sort Source # | |||||
Suggest Term Source # | |||||
Defined in Agda.Syntax.Internal suggestName :: Term -> Maybe String Source # | |||||
TelToArgs ListTel Source # | |||||
TelToArgs Telescope Source # | |||||
TermSize Level Source # | |||||
TermSize PlusLevel Source # | |||||
TermSize Sort Source # | |||||
TermSize Term Source # | |||||
GetDefs Level Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Level -> m () Source # | |||||
GetDefs PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => PlusLevel -> m () Source # | |||||
GetDefs Sort Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Sort -> m () Source # | |||||
GetDefs Telescope Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Telescope -> m () Source # | |||||
GetDefs Term Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Term -> m () Source # | |||||
GetDefs Type Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Type -> m () Source # | |||||
TermLike Level Source # | |||||
TermLike PlusLevel Source # | |||||
TermLike Sort Source # | |||||
TermLike Term Source # | |||||
TermLike Type Source # | |||||
AllMetas Level Source # | |||||
AllMetas PlusLevel Source # | |||||
AllMetas Sort Source # | |||||
AllMetas Term Source # | |||||
AllMetas Type Source # | |||||
NamesIn Level Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
NamesIn PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
NamesIn Sort Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
NamesIn Term Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
NamesIn CompiledClauses Source # | |||||
Defined in Agda.Syntax.Internal.Names namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompiledClauses -> m Source # | |||||
KillRange Level Source # | |||||
Defined in Agda.Syntax.Internal | |||||
KillRange PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal | |||||
KillRange Sort Source # | |||||
Defined in Agda.Syntax.Internal | |||||
KillRange Substitution Source # | |||||
Defined in Agda.Syntax.Internal | |||||
KillRange Term Source # | |||||
Defined in Agda.Syntax.Internal | |||||
KillRange CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.CompiledClause | |||||
Reify Level Source # | |||||
Reify Sort Source # | |||||
Reify Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract
| |||||
Reify Term Source # | |||||
Reify Type Source # | |||||
TerSetSizeDepth ListTel Source # | |||||
Defined in Agda.Termination.Monad | |||||
TerSetSizeDepth Telescope Source # | |||||
Defined in Agda.Termination.Monad | |||||
AbsTerm Level Source # | |||||
AbsTerm PlusLevel Source # | |||||
AbsTerm Sort Source # | |||||
AbsTerm Term Source # | |||||
AbsTerm Type Source # | |||||
EqualSy Level Source # | |||||
EqualSy PlusLevel Source # | |||||
EqualSy Sort Source # | |||||
EqualSy Term Source # | |||||
EqualSy Type Source # | Ignores sorts. | ||||
IsPrefixOf Args Source # | |||||
Defined in Agda.TypeChecking.Abstract | |||||
IsPrefixOf Elims Source # | |||||
Defined in Agda.TypeChecking.Abstract | |||||
IsPrefixOf Term Source # | |||||
Defined in Agda.TypeChecking.Abstract | |||||
CheckInternal Elims Source # | |||||
Defined in Agda.TypeChecking.CheckInternal checkInternal' :: MonadCheckInternal m => Action m -> Elims -> Comparison -> TypeOf Elims -> m Elims Source # checkInternal :: MonadCheckInternal m => Elims -> Comparison -> TypeOf Elims -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Action m -> Elims -> m Elims Source # inferInternal :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Elims -> m () Source # | |||||
CheckInternal Level Source # | |||||
Defined in Agda.TypeChecking.CheckInternal checkInternal' :: MonadCheckInternal m => Action m -> Level -> Comparison -> TypeOf Level -> m Level Source # checkInternal :: MonadCheckInternal m => Level -> Comparison -> TypeOf Level -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Level ~ ()) => Action m -> Level -> m Level Source # inferInternal :: (MonadCheckInternal m, TypeOf Level ~ ()) => Level -> m () Source # | |||||
CheckInternal PlusLevel Source # | |||||
Defined in Agda.TypeChecking.CheckInternal checkInternal' :: MonadCheckInternal m => Action m -> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel Source # checkInternal :: MonadCheckInternal m => PlusLevel -> Comparison -> TypeOf PlusLevel -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => Action m -> PlusLevel -> m PlusLevel Source # inferInternal :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => PlusLevel -> m () Source # | |||||
CheckInternal Sort Source # | |||||
Defined in Agda.TypeChecking.CheckInternal checkInternal' :: MonadCheckInternal m => Action m -> Sort -> Comparison -> TypeOf Sort -> m Sort Source # checkInternal :: MonadCheckInternal m => Sort -> Comparison -> TypeOf Sort -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Action m -> Sort -> m Sort Source # inferInternal :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Sort -> m () Source # | |||||
CheckInternal Term Source # | |||||
Defined in Agda.TypeChecking.CheckInternal checkInternal' :: MonadCheckInternal m => Action m -> Term -> Comparison -> TypeOf Term -> m Term Source # checkInternal :: MonadCheckInternal m => Term -> Comparison -> TypeOf Term -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Term ~ ()) => Action m -> Term -> m Term Source # inferInternal :: (MonadCheckInternal m, TypeOf Term ~ ()) => Term -> m () Source # | |||||
CheckInternal Type Source # | |||||
Defined in Agda.TypeChecking.CheckInternal checkInternal' :: MonadCheckInternal m => Action m -> Type -> Comparison -> TypeOf Type -> m Type Source # checkInternal :: MonadCheckInternal m => Type -> Comparison -> TypeOf Type -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Type ~ ()) => Action m -> Type -> m Type Source # inferInternal :: (MonadCheckInternal m, TypeOf Type ~ ()) => Type -> m () Source # | |||||
DropArgs Telescope Source # | NOTE: This creates telescopes with unbound de Bruijn indices. | ||||
DropArgs Term Source # | Use for dropping initial lambdas in clause bodies. NOTE: does not reduce term, need lambdas to be present. | ||||
DropArgs CompiledClauses Source # | To drop the first | ||||
Defined in Agda.TypeChecking.DropArgs dropArgs :: Int -> CompiledClauses -> CompiledClauses Source # | |||||
Free Level Source # | |||||
Free Sort Source # | |||||
Free Term Source # | |||||
PrecomputeFreeVars Level Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: Level -> FV Level Source # | |||||
PrecomputeFreeVars PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: PlusLevel -> FV PlusLevel Source # | |||||
PrecomputeFreeVars Sort Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: Sort -> FV Sort Source # | |||||
PrecomputeFreeVars Term Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: Term -> FV Term Source # | |||||
PrecomputeFreeVars Type Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: Type -> FV Type Source # | |||||
ForceNotFree Level Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => Level -> m Level | |||||
ForceNotFree PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel | |||||
ForceNotFree Sort Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => Sort -> m Sort | |||||
ForceNotFree Term Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => Term -> m Term | |||||
ForceNotFree Type Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => Type -> m Type | |||||
UsableModality Level Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Level -> m Bool Source # | |||||
UsableModality Sort Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Sort -> m Bool Source # | |||||
UsableModality Term Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Term -> m Bool Source # | |||||
UsableRelevance Level Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Level -> m Bool Source # | |||||
UsableRelevance PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> PlusLevel -> m Bool Source # | |||||
UsableRelevance Sort Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Sort -> m Bool Source # | |||||
UsableRelevance Term Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Term -> m Bool Source # | |||||
NoProjectedVar Term Source # | |||||
Defined in Agda.TypeChecking.MetaVars noProjectedVar :: Term -> Either ProjectedVar () Source # | |||||
ReduceAndEtaContract Term Source # | |||||
Defined in Agda.TypeChecking.MetaVars | |||||
MentionsMeta Elim Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Elim -> Bool Source # | |||||
MentionsMeta Level Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Level -> Bool Source # | |||||
MentionsMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool Source # | |||||
MentionsMeta Sort Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Sort -> Bool Source # | |||||
MentionsMeta Term Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Term -> Bool Source # | |||||
MentionsMeta Type Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Type -> Bool Source # | |||||
AnyRigid Level Source # | |||||
AnyRigid PlusLevel Source # | |||||
AnyRigid Sort Source # | |||||
AnyRigid Term Source # | |||||
AnyRigid Type Source # | |||||
Occurs Elims Source # | |||||
Occurs Level Source # | |||||
Occurs PlusLevel Source # | |||||
Occurs Sort Source # | |||||
Occurs Term Source # | |||||
Occurs Type Source # | |||||
AddContext Telescope Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => Telescope -> m a -> m a Source # contextSize :: Telescope -> Nat Source # | |||||
IsInstantiatedMeta Level Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Level -> m Bool Source # | |||||
IsInstantiatedMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars isInstantiatedMeta :: (MonadFail m, ReadTCState m) => PlusLevel -> m Bool Source # | |||||
IsInstantiatedMeta Term Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Term -> m Bool Source # | |||||
UnFreezeMeta Level Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => Level -> m () Source # | |||||
UnFreezeMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => PlusLevel -> m () Source # | |||||
UnFreezeMeta Sort Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source # | |||||
UnFreezeMeta Term Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => Term -> m () Source # | |||||
UnFreezeMeta Type Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => Type -> m () Source # | |||||
IsSizeType Term Source # | |||||
Defined in Agda.TypeChecking.Monad.SizedTypes isSizeType :: (HasOptions m, HasBuiltins m) => Term -> m (Maybe BoundedSize) Source # | |||||
ComputeOccurrences Level Source # | |||||
Defined in Agda.TypeChecking.Positivity | |||||
ComputeOccurrences PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Positivity | |||||
ComputeOccurrences Term Source # | |||||
Defined in Agda.TypeChecking.Positivity occurrences :: Term -> OccM OccurrencesBuilder Source # | |||||
ComputeOccurrences Type Source # | |||||
Defined in Agda.TypeChecking.Positivity occurrences :: Type -> OccM OccurrencesBuilder Source # | |||||
PrettyTCM Elim Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM Level Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM Sort Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM Telescope Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM Term Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM Type Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM ContextEntry Source # | |||||
Defined in Agda.TypeChecking.Pretty prettyTCM :: MonadPretty m => ContextEntry -> m Doc Source # | |||||
PrimTerm Type Source # | |||||
PrimType Type Source # | |||||
ToTerm Term Source # | |||||
ToTerm Type Source # | |||||
Instantiate Level Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Instantiate Sort Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Instantiate Term Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull Level Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull Sort Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull Substitution Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull Term Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
IsMeta Term Source # | |||||
Normalise Level Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise Sort Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise Term Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Reduce Elim Source # | |||||
Reduce Level Source # | |||||
Reduce PlusLevel Source # | |||||
Reduce Sort Source # | |||||
Reduce Telescope Source # | |||||
Reduce Term Source # | |||||
Reduce Type Source # | |||||
Simplify Level Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Simplify PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Simplify Sort Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Simplify Term Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
GetMatchables Term Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern getMatchables :: Term -> [QName] Source # | |||||
EmbPrj Blocked_ Source # | |||||
EmbPrj Level Source # | |||||
EmbPrj NotBlocked Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Internal icode :: NotBlocked -> S Int32 Source # icod_ :: NotBlocked -> S Int32 Source # value :: Int32 -> R NotBlocked Source # | |||||
EmbPrj PlusLevel Source # | |||||
EmbPrj Sort Source # | |||||
EmbPrj Term Source # | |||||
EmbPrj CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Internal icode :: CompiledClauses -> S Int32 Source # icod_ :: CompiledClauses -> S Int32 Source # value :: Int32 -> R CompiledClauses Source # | |||||
TeleNoAbs ListTel Source # | |||||
TeleNoAbs Telescope Source # | |||||
Abstract Sort Source # | |||||
Abstract Telescope Source # | |||||
Abstract Term Source # | |||||
Abstract Type Source # | |||||
Abstract CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.Substitute abstract :: Telescope -> CompiledClauses -> CompiledClauses Source # | |||||
Apply Sort Source # | |||||
Apply Term Source # | |||||
Apply CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.Substitute apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source # | |||||
Subst Term Source # | |||||
Defined in Agda.TypeChecking.Substitute applySubst :: Substitution' (SubstArg Term) -> Term -> Term Source # | |||||
DeBruijn Level Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn deBruijnVar :: Int -> Level Source # debruijnNamedVar :: String -> Int -> Level Source # deBruijnView :: Level -> Maybe Int Source # | |||||
DeBruijn PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn deBruijnVar :: Int -> PlusLevel Source # debruijnNamedVar :: String -> Int -> PlusLevel Source # deBruijnView :: PlusLevel -> Maybe Int Source # | |||||
DeBruijn Term Source # | We can substitute | ||||
Defined in Agda.TypeChecking.Substitute.DeBruijn deBruijnVar :: Int -> Term Source # debruijnNamedVar :: String -> Int -> Term Source # deBruijnView :: Term -> Maybe Int Source # | |||||
SynEq Level Source # | |||||
SynEq PlusLevel Source # | |||||
SynEq Sort Source # | |||||
SynEq Term Source # | Syntactic term equality ignores | ||||
SynEq Type Source # | Syntactic equality ignores sorts. | ||||
PiApplyM Term Source # | |||||
Defined in Agda.TypeChecking.Telescope piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Term -> m Type Source # piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Term -> m Type Source # | |||||
NFData Level Source # | |||||
Defined in Agda.Syntax.Internal | |||||
NFData PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal | |||||
NFData Sort Source # | |||||
Defined in Agda.Syntax.Internal | |||||
NFData Term Source # | |||||
Defined in Agda.Syntax.Internal | |||||
NFData Type Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Show Term Source # | |||||
Eq Level | |||||
Eq NotBlocked | |||||
Defined in Agda.TypeChecking.Substitute (==) :: NotBlocked -> NotBlocked -> Bool (/=) :: NotBlocked -> NotBlocked -> Bool | |||||
Eq PlusLevel | |||||
Eq Sort | |||||
Eq Substitution | |||||
Defined in Agda.TypeChecking.Substitute (==) :: Substitution -> Substitution -> Bool (/=) :: Substitution -> Substitution -> Bool | |||||
Eq Term | Syntactic | ||||
Eq SingleLevel | |||||
Defined in Agda.TypeChecking.Level (==) :: SingleLevel -> SingleLevel -> Bool (/=) :: SingleLevel -> SingleLevel -> Bool | |||||
Ord Level | |||||
Ord PlusLevel | |||||
Defined in Agda.TypeChecking.Substitute | |||||
Ord Sort | |||||
Ord Substitution | |||||
Defined in Agda.TypeChecking.Substitute compare :: Substitution -> Substitution -> Ordering (<) :: Substitution -> Substitution -> Bool (<=) :: Substitution -> Substitution -> Bool (>) :: Substitution -> Substitution -> Bool (>=) :: Substitution -> Substitution -> Bool max :: Substitution -> Substitution -> Substitution min :: Substitution -> Substitution -> Substitution | |||||
Ord Term | |||||
Match NLPSort Sort Source # | |||||
Match NLPType Type Source # | |||||
Match NLPat Level Source # | |||||
Match NLPat Term Source # | |||||
NLPatToTerm Nat Term Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
NLPatToTerm NLPSort Sort Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
NLPatToTerm NLPType Type Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
NLPatToTerm NLPat Level Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
NLPatToTerm NLPat Term Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
PatternFrom Level NLPat Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
PatternFrom Sort NLPSort Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
PatternFrom Term NLPat Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
PatternFrom Type NLPType Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
MonadError Blocked_ NLM | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinMatch throwError :: Blocked_ -> NLM a catchError :: NLM a -> (Blocked_ -> NLM a) -> NLM a | |||||
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Internal | |||||
PatternFrom Elims [Elim' NLPat] Source # | |||||
Pretty a => Pretty (Blocked a) Source # | |||||
Pretty a => Pretty (Tele (Dom a)) Source # | |||||
LensSort a => LensSort (Dom a) Source # | |||||
LensSort (Type' a) Source # | |||||
SgTel (Dom Type) Source # | |||||
SgTel (Dom (ArgName, Type)) Source # | |||||
GetDefs a => GetDefs (Dom a) Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Dom a -> m () Source # | |||||
TermLike a => TermLike (Blocked a) Source # | |||||
TermLike a => TermLike (Dom a) Source # | |||||
NamesIn a => NamesIn (Type' a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
KillRange a => KillRange (Blocked a) Source # | |||||
Defined in Agda.Syntax.Internal killRange :: KillRangeT (Blocked a) Source # | |||||
KillRange a => KillRange (Type' a) Source # | |||||
Defined in Agda.Syntax.Internal killRange :: KillRangeT (Type' a) Source # | |||||
Reify i => Reify (Dom i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract
| |||||
AbsTerm a => AbsTerm (Dom a) Source # | |||||
EqualSy a => EqualSy (Dom a) Source # | Ignore the tactic. | ||||
Free t => Free (Dom t) Source # | |||||
Free t => Free (Type' t) Source # | |||||
PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: Dom a -> FV (Dom a) Source # | |||||
(Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => Dom a -> m (Dom a) | |||||
UsableModality a => UsableModality (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Dom a -> m Bool Source # | |||||
UsableRelevance a => UsableModality (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Type' a -> m Bool Source # | |||||
UsableRelevance a => UsableRelevance (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Dom a -> m Bool Source # | |||||
UsableRelevance a => UsableRelevance (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Type' a -> m Bool Source # | |||||
MentionsMeta t => MentionsMeta (Dom t) Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Dom t -> Bool Source # | |||||
AnyRigid a => AnyRigid (Dom a) Source # | |||||
Occurs (Abs Term) Source # | |||||
Occurs (Abs Type) Source # | |||||
Occurs a => Occurs (Dom a) Source # | |||||
AddContext (Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => Dom Type -> m a -> m a Source # | |||||
AddContext (Dom (Name, Type)) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source # | |||||
AddContext (Dom (String, Type)) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source # | |||||
AddContext (KeepNames Telescope) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # | |||||
IsSizeType a => IsSizeType (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Monad.SizedTypes isSizeType :: (HasOptions m, HasBuiltins m) => Dom a -> m (Maybe BoundedSize) Source # | |||||
IsSizeType a => IsSizeType (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Monad.SizedTypes isSizeType :: (HasOptions m, HasBuiltins m) => Type' a -> m (Maybe BoundedSize) Source # | |||||
ComputeOccurrences a => ComputeOccurrences (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Positivity occurrences :: Dom a -> OccM OccurrencesBuilder Source # | |||||
PrettyTCM (Arg Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Arg Type) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (NamedArg Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Named_ Term) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM a => PrettyTCM (Blocked a) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Type' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
ToTerm (Dom Type) Source # | |||||
Instantiate a => Instantiate (Blocked a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Instantiate t => Instantiate (Type' t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull t => InstantiateFull (Type' t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise t => Normalise (Dom t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise t => Normalise (Type' t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Reduce t => Reduce (Dom t) Source # | |||||
Simplify t => Simplify (Dom t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Simplify t => Simplify (Type' t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
GetMatchables a => GetMatchables (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern getMatchables :: Dom a -> [QName] Source # | |||||
EmbPrj a => EmbPrj (Dom a) Source # | |||||
EmbPrj a => EmbPrj (Type' a) Source # | |||||
Apply t => Apply (Blocked t) Source # | |||||
Subst a => Subst (Blocked a) Source # | |||||
Defined in Agda.TypeChecking.Substitute
applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a Source # | |||||
SynEq a => SynEq (Dom a) Source # | |||||
Unquote a => Unquote (Dom a) Source # | |||||
NFData e => NFData (Dom e) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Eq t => Eq (Blocked t) | |||||
Eq a => Eq (Type' a) | Syntactic | ||||
Ord a => Ord (Dom a) | |||||
Ord a => Ord (Type' a) | |||||
Match [Elim' NLPat] Elims Source # | |||||
ToNLPat a b => ToNLPat (Dom a) (Dom b) Source # | |||||
Match a b => Match (Dom a) (Dom b) Source # | |||||
NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
PatternFrom a b => PatternFrom (Dom a) (Dom b) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
SgTel (ArgName, Dom Type) Source # | |||||
(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract
toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name)) Source # | |||||
AddContext (Name, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source # | |||||
AddContext (KeepNames String, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a Source # | |||||
AddContext (List1 Name, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext (List1 (Arg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext (List1 (WithHiding Name), Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat Source # | |||||
AddContext (Text, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source # | |||||
AddContext (String, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source # | |||||
AddContext ([Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source # | |||||
AddContext ([Arg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # | |||||
AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
AddContext ([WithHiding Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source # | |||||
type TypeOf Elims Source # | |||||
type TypeOf Level Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type TypeOf PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type TypeOf Sort Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type TypeOf Term Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type TypeOf Type Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type ReifiesTo Level Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type ReifiesTo Sort Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type ReifiesTo Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type ReifiesTo Term Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type ReifiesTo Type Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type SubstArg Term Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type TypeOf (Abs Term) Source # | |||||
type TypeOf (Abs Type) Source # | |||||
type TypeOf (Dom a) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type TypeOf [PlusLevel] Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type ReifiesTo (Dom i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type SubstArg (Blocked a) Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type AbsOfRef (Dom r, Name) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract |
= Pattern' PatVarName | The |
A clause is a list of patterns and the clause body.
The telescope contains the types of the pattern variables and the de Bruijn indices say how to get from the order the variables occur in the patterns to the order they occur in the telescope. The body binds the variables in the order they appear in the telescope.
clauseTel ~ permute clausePerm (patternVars namedClausePats)
Terms in dot patterns are valid in the clause telescope.
For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!
Clause | |
|
Instances
Pretty Clause Source # | |||||
GetDefs Clause Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Clause -> m () Source # | |||||
NamesIn Clause Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
FunArity Clause Source # | Get the number of initial | ||||
Defined in Agda.Syntax.Internal.Pattern | |||||
HasRange Clause Source # | |||||
KillRange Clause Source # | |||||
Defined in Agda.Syntax.Internal | |||||
DropArgs Clause Source # | NOTE: does not work for recursive functions. | ||||
DropArgs FunctionInverse Source # | |||||
Defined in Agda.TypeChecking.DropArgs dropArgs :: Int -> FunctionInverse -> FunctionInverse Source # | |||||
Free Clause Source # | |||||
Occurs Clause Source # | |||||
ComputeOccurrences Clause Source # | |||||
Defined in Agda.TypeChecking.Positivity | |||||
PrettyTCM Clause Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
NormaliseProjP Clause Source # | |||||
Defined in Agda.TypeChecking.Records normaliseProjP :: HasConstInfo m => Clause -> m Clause Source # | |||||
InstantiateFull Clause Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull FunctionInverse Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj Clause Source # | |||||
Abstract Clause Source # | |||||
Abstract FunctionInverse Source # | |||||
Defined in Agda.TypeChecking.Substitute abstract :: Telescope -> FunctionInverse -> FunctionInverse Source # | |||||
Apply Clause Source # | |||||
Apply FunctionInverse Source # | |||||
Defined in Agda.TypeChecking.Substitute apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source # | |||||
Null Clause Source # | A | ||||
NFData Clause Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Generic Clause Source # | |||||
Defined in Agda.Syntax.Internal
| |||||
Show Clause Source # | |||||
FunArity [Clause] Source # | Get the number of common initial | ||||
Defined in Agda.Syntax.Internal.Pattern | |||||
Reify (QNamed Clause) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract
| |||||
PrettyTCM (QNamed Clause) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
type Rep Clause Source # | |||||
Defined in Agda.Syntax.Internal type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) (((S1 ('MetaSel ('Just "clauseLHSRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Just "clauseFullRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "clauseTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope))) :*: (S1 ('MetaSel ('Just "namedClausePats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NAPs) :*: (S1 ('MetaSel ('Just "clauseBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Term)) :*: S1 ('MetaSel ('Just "clauseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type)))))) :*: ((S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "clauseExact") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: S1 ('MetaSel ('Just "clauseRecursive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)))) :*: (S1 ('MetaSel ('Just "clauseUnreachable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: (S1 ('MetaSel ('Just "clauseEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis) :*: S1 ('MetaSel ('Just "clauseWhereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName))))))) | |||||
type ReifiesTo (QNamed Clause) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract |
Sorts.
Univ Univ (Level' t) |
|
Inf Univ !Integer |
|
SizeUniv |
|
LockUniv |
|
LevelUniv |
|
IntervalUniv |
|
PiSort (Dom' t t) (Sort' t) (Abs (Sort' t)) | Sort of the pi type. |
FunSort (Sort' t) (Sort' t) | Sort of a (non-dependent) function type. |
UnivSort (Sort' t) | Sort of another sort. |
MetaS !MetaId [Elim' t] | |
DefS QName [Elim' t] | A postulated sort. |
DummyS String | A (part of a) term or type which is only used for internal purposes.
Replaces the abuse of |
Instances
Pretty Sort Source # | |||||
LensSort Sort Source # | |||||
TermSize Sort Source # | |||||
GetDefs Sort Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Sort -> m () Source # | |||||
TermLike Sort Source # | |||||
AllMetas Sort Source # | |||||
NamesIn Sort Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
KillRange Sort Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Reify Sort Source # | |||||
AbsTerm Sort Source # | |||||
EqualSy Sort Source # | |||||
CheckInternal Sort Source # | |||||
Defined in Agda.TypeChecking.CheckInternal checkInternal' :: MonadCheckInternal m => Action m -> Sort -> Comparison -> TypeOf Sort -> m Sort Source # checkInternal :: MonadCheckInternal m => Sort -> Comparison -> TypeOf Sort -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Action m -> Sort -> m Sort Source # inferInternal :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Sort -> m () Source # | |||||
Free Sort Source # | |||||
PrecomputeFreeVars Sort Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: Sort -> FV Sort Source # | |||||
ForceNotFree Sort Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => Sort -> m Sort | |||||
UsableModality Sort Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Sort -> m Bool Source # | |||||
UsableRelevance Sort Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Sort -> m Bool Source # | |||||
MentionsMeta Sort Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Sort -> Bool Source # | |||||
AnyRigid Sort Source # | |||||
Occurs Sort Source # | |||||
UnFreezeMeta Sort Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source # | |||||
PrettyTCM Sort Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
Instantiate Sort Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull Sort Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise Sort Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Reduce Sort Source # | |||||
Simplify Sort Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj Sort Source # | |||||
Abstract Sort Source # | |||||
Apply Sort Source # | |||||
SynEq Sort Source # | |||||
NFData Sort Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Eq Sort | |||||
Ord Sort | |||||
Match NLPSort Sort Source # | |||||
NLPatToTerm NLPSort Sort Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
PatternFrom Sort NLPSort Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
IsMeta a => IsMeta (Sort' a) Source # | |||||
(Coercible a Term, Subst a) => Subst (Sort' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute
applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a Source # | |||||
Show t => Show (Sort' t) Source # | |||||
type TypeOf Sort Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type ReifiesTo Sort Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type SubstArg (Sort' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute |
class PatternVars a where Source #
Extract pattern variables in left-to-right order.
A DotP
is also treated as variable (see docu for Clause
).
type PatternVarOut a Source #
patternVars :: a -> [Arg (Either (PatternVarOut a) Term)] Source #
Instances
PatternVars (Arg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal
patternVars :: Arg (Pattern' a) -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)] Source # | |||||
PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal
patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source # | |||||
PatternVars a => PatternVars [a] Source # | |||||
Defined in Agda.Syntax.Internal
patternVars :: [a] -> [Arg (Either (PatternVarOut [a]) Term)] Source # |
data Substitution' a Source #
Substitutions.
IdS | Identity substitution.
|
EmptyS Impossible | Empty substitution, lifts from the empty context. First argument is |
a :# (Substitution' a) infixr 4 | Substitution extension, ` |
Strengthen Impossible !Int (Substitution' a) | Strengthening substitution. First argument is |
Wk !Int (Substitution' a) | Weakening substitution, lifts to an extended context.
|
Lift !Int (Substitution' a) | Lifting substitution. Use this to go under a binder.
|
Instances
KillRange Substitution Source # | |||||
Defined in Agda.Syntax.Internal | |||||
InstantiateFull Substitution Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Functor Substitution' Source # | |||||
Defined in Agda.Syntax.Internal fmap :: (a -> b) -> Substitution' a -> Substitution' b (<$) :: a -> Substitution' b -> Substitution' a # | |||||
Foldable Substitution' Source # | |||||
Defined in Agda.Syntax.Internal fold :: Monoid m => Substitution' m -> m foldMap :: Monoid m => (a -> m) -> Substitution' a -> m foldMap' :: Monoid m => (a -> m) -> Substitution' a -> m foldr :: (a -> b -> b) -> b -> Substitution' a -> b foldr' :: (a -> b -> b) -> b -> Substitution' a -> b foldl :: (b -> a -> b) -> b -> Substitution' a -> b foldl' :: (b -> a -> b) -> b -> Substitution' a -> b foldr1 :: (a -> a -> a) -> Substitution' a -> a foldl1 :: (a -> a -> a) -> Substitution' a -> a toList :: Substitution' a -> [a] null :: Substitution' a -> Bool length :: Substitution' a -> Int elem :: Eq a => a -> Substitution' a -> Bool maximum :: Ord a => Substitution' a -> a minimum :: Ord a => Substitution' a -> a sum :: Num a => Substitution' a -> a product :: Num a => Substitution' a -> a | |||||
Traversable Substitution' Source # | |||||
Defined in Agda.Syntax.Internal traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) | |||||
Eq Substitution | |||||
Defined in Agda.TypeChecking.Substitute (==) :: Substitution -> Substitution -> Bool (/=) :: Substitution -> Substitution -> Bool | |||||
Ord Substitution | |||||
Defined in Agda.TypeChecking.Substitute compare :: Substitution -> Substitution -> Ordering (<) :: Substitution -> Substitution -> Bool (<=) :: Substitution -> Substitution -> Bool (>) :: Substitution -> Substitution -> Bool (>=) :: Substitution -> Substitution -> Bool max :: Substitution -> Substitution -> Substitution min :: Substitution -> Substitution -> Substitution | |||||
Pretty a => Pretty (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal pretty :: Substitution' a -> Doc Source # prettyPrec :: Int -> Substitution' a -> Doc Source # prettyList :: [Substitution' a] -> Doc Source # | |||||
TermSize a => TermSize (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal termSize :: Substitution' a -> Int Source # tsize :: Substitution' a -> Sum Int Source # | |||||
NamesIn a => NamesIn (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal.Names namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Substitution' a -> m Source # | |||||
(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source # | |||||
Defined in Agda.TypeChecking.Pretty prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source # | |||||
EmbPrj a => EmbPrj (Substitution' a) Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Internal icode :: Substitution' a -> S Int32 Source # icod_ :: Substitution' a -> S Int32 Source # value :: Int32 -> R (Substitution' a) Source # | |||||
EndoSubst a => Subst (Substitution' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute
applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source # | |||||
Null (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal empty :: Substitution' a Source # null :: Substitution' a -> Bool Source # | |||||
NFData a => NFData (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal rnf :: Substitution' a -> () | |||||
Generic (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal
from :: Substitution' a -> Rep (Substitution' a) x to :: Rep (Substitution' a) x -> Substitution' a | |||||
Show a => Show (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal showsPrec :: Int -> Substitution' a -> ShowS show :: Substitution' a -> String showList :: [Substitution' a] -> ShowS | |||||
type SubstArg (Substitution' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type Rep (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))))) |
Binder.
Abs
: The bound variable might appear in the body.
NoAbs
is pseudo-binder, it does not introduce a fresh variable,
similar to the const
of Haskell.
Instances
Decoration Abs Source # | |||||
Functor Abs Source # | |||||
Foldable Abs Source # | |||||
Defined in Agda.Syntax.Internal fold :: Monoid m => Abs m -> m foldMap :: Monoid m => (a -> m) -> Abs a -> m foldMap' :: Monoid m => (a -> m) -> Abs a -> m foldr :: (a -> b -> b) -> b -> Abs a -> b foldr' :: (a -> b -> b) -> b -> Abs a -> b foldl :: (b -> a -> b) -> b -> Abs a -> b foldl' :: (b -> a -> b) -> b -> Abs a -> b foldr1 :: (a -> a -> a) -> Abs a -> a foldl1 :: (a -> a -> a) -> Abs a -> a elem :: Eq a => a -> Abs a -> Bool maximum :: Ord a => Abs a -> a | |||||
Traversable Abs Source # | |||||
Pretty t => Pretty (Abs t) Source # | |||||
Suggest (Abs b) Source # | |||||
Defined in Agda.Syntax.Internal suggestName :: Abs b -> Maybe String Source # | |||||
GetDefs a => GetDefs (Abs a) Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Abs a -> m () Source # | |||||
TermLike a => TermLike (Abs a) Source # | |||||
NamesIn a => NamesIn (Abs a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
KillRange a => KillRange (Abs a) Source # | |||||
Defined in Agda.Syntax.Internal killRange :: KillRangeT (Abs a) Source # | |||||
(Free i, Reify i) => Reify (Abs i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract
| |||||
(TermSubst a, AbsTerm a) => AbsTerm (Abs a) Source # | |||||
(Subst a, EqualSy a) => EqualSy (Abs a) Source # | Ignores | ||||
Free t => Free (Abs t) Source # | |||||
PrecomputeFreeVars a => PrecomputeFreeVars (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: Abs a -> FV (Abs a) Source # | |||||
(Reduce a, ForceNotFree a) => ForceNotFree (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => Abs a -> m (Abs a) | |||||
(Subst a, UsableRelevance a) => UsableRelevance (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Abs a -> m Bool Source # | |||||
MentionsMeta t => MentionsMeta (Abs t) Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Abs t -> Bool Source # | |||||
(Subst a, AnyRigid a) => AnyRigid (Abs a) Source # | |||||
Occurs (Abs Term) Source # | |||||
Occurs (Abs Type) Source # | |||||
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source # | Does not worry about raising. | ||||
Defined in Agda.TypeChecking.Monad.MetaVars isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Abs a -> m Bool Source # | |||||
UnFreezeMeta a => UnFreezeMeta (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => Abs a -> m () Source # | |||||
ComputeOccurrences a => ComputeOccurrences (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Positivity occurrences :: Abs a -> OccM OccurrencesBuilder Source # | |||||
Instantiate t => Instantiate (Abs t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
(Subst a, InstantiateFull a) => InstantiateFull (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
(Subst a, Normalise a) => Normalise (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
(Subst a, Reduce a) => Reduce (Abs a) Source # | |||||
(Subst a, Simplify a) => Simplify (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
GetMatchables a => GetMatchables (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern getMatchables :: Abs a -> [QName] Source # | |||||
NLPatVars a => NLPatVars (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
EmbPrj a => EmbPrj (Abs a) Source # | |||||
Subst a => Subst (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Substitute applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source # | |||||
(Subst a, SynEq a) => SynEq (Abs a) Source # | |||||
Sized a => Sized (Abs a) Source # | |||||
NFData a => NFData (Abs a) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Generic (Abs a) Source # | |||||
Defined in Agda.Syntax.Internal
| |||||
Show a => Show (Abs a) Source # | |||||
(Subst a, Eq a) => Eq (Abs a) | Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution. | ||||
(Subst a, Ord a) => Ord (Abs a) | |||||
ToNLPat a b => ToNLPat (Abs a) (Abs b) Source # | |||||
NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
type TypeOf (Abs Term) Source # | |||||
type TypeOf (Abs Type) Source # | |||||
type ReifiesTo (Abs i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type SubstArg (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type Rep (Abs a) Source # | |||||
Defined in Agda.Syntax.Internal type Rep (Abs a) = D1 ('MetaData "Abs" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Abs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "NoAbs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))) |
A level is a maximum expression of a closed level and 0..n
PlusLevel
expressions each of which is an atom plus a number.
Max !Integer [PlusLevel' t] |
Instances
Pretty Level Source # | |||||
TermSize Level Source # | |||||
GetDefs Level Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Level -> m () Source # | |||||
TermLike Level Source # | |||||
AllMetas Level Source # | |||||
NamesIn Level Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
KillRange Level Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Reify Level Source # | |||||
AbsTerm Level Source # | |||||
EqualSy Level Source # | |||||
CheckInternal Level Source # | |||||
Defined in Agda.TypeChecking.CheckInternal checkInternal' :: MonadCheckInternal m => Action m -> Level -> Comparison -> TypeOf Level -> m Level Source # checkInternal :: MonadCheckInternal m => Level -> Comparison -> TypeOf Level -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Level ~ ()) => Action m -> Level -> m Level Source # inferInternal :: (MonadCheckInternal m, TypeOf Level ~ ()) => Level -> m () Source # | |||||
Free Level Source # | |||||
PrecomputeFreeVars Level Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: Level -> FV Level Source # | |||||
ForceNotFree Level Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => Level -> m Level | |||||
UsableModality Level Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Level -> m Bool Source # | |||||
UsableRelevance Level Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Level -> m Bool Source # | |||||
MentionsMeta Level Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Level -> Bool Source # | |||||
AnyRigid Level Source # | |||||
Occurs Level Source # | |||||
IsInstantiatedMeta Level Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Level -> m Bool Source # | |||||
UnFreezeMeta Level Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => Level -> m () Source # | |||||
ComputeOccurrences Level Source # | |||||
Defined in Agda.TypeChecking.Positivity | |||||
PrettyTCM Level Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
Instantiate Level Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull Level Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise Level Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Reduce Level Source # | |||||
Simplify Level Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj Level Source # | |||||
DeBruijn Level Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn deBruijnVar :: Int -> Level Source # debruijnNamedVar :: String -> Int -> Level Source # deBruijnView :: Level -> Maybe Int Source # | |||||
SynEq Level Source # | |||||
NFData Level Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Functor Level' Source # | |||||
Foldable Level' Source # | |||||
Defined in Agda.Syntax.Internal fold :: Monoid m => Level' m -> m foldMap :: Monoid m => (a -> m) -> Level' a -> m foldMap' :: Monoid m => (a -> m) -> Level' a -> m foldr :: (a -> b -> b) -> b -> Level' a -> b foldr' :: (a -> b -> b) -> b -> Level' a -> b foldl :: (b -> a -> b) -> b -> Level' a -> b foldl' :: (b -> a -> b) -> b -> Level' a -> b foldr1 :: (a -> a -> a) -> Level' a -> a foldl1 :: (a -> a -> a) -> Level' a -> a elem :: Eq a => a -> Level' a -> Bool maximum :: Ord a => Level' a -> a | |||||
Traversable Level' Source # | |||||
Eq Level | |||||
Ord Level | |||||
Match NLPat Level Source # | |||||
NLPatToTerm NLPat Level Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
PatternFrom Level NLPat Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
IsMeta a => IsMeta (Level' a) Source # | |||||
Subst a => Subst (Level' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute
applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a Source # | |||||
Show t => Show (Level' t) Source # | |||||
type TypeOf Level Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type ReifiesTo Level Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type SubstArg (Level' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute |
Store the names of the record fields in the constructor. This allows reduction of projection redexes outside of TCM. For instance, during substitution and application.
ConHead | |
|
Instances
CopatternMatchingAllowed ConHead Source # | |||||
Defined in Agda.Syntax.Internal copatternMatchingAllowed :: ConHead -> Bool Source # | |||||
Pretty ConHead Source # | |||||
LensConName ConHead Source # | |||||
Defined in Agda.Syntax.Internal | |||||
NamesIn ConHead Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
HasRange ConHead Source # | |||||
KillRange ConHead Source # | |||||
Defined in Agda.Syntax.Internal | |||||
SetRange ConHead Source # | |||||
PrettyTCM ConHead Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
InstantiateFull ConHead Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj ConHead Source # | |||||
NFData ConHead Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Generic ConHead Source # | |||||
Defined in Agda.Syntax.Internal
| |||||
Show ConHead Source # | |||||
Eq ConHead Source # | |||||
Ord ConHead Source # | |||||
type Rep ConHead Source # | |||||
Defined in Agda.Syntax.Internal type Rep ConHead = D1 ('MetaData "ConHead" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ConHead" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "conDataRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataOrRecord)) :*: (S1 ('MetaSel ('Just "conInductive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction) :*: S1 ('MetaSel ('Just "conFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg QName])))) |
data PlusLevel' t Source #
Plus !Integer t |
Instances
Pretty PlusLevel Source # | |||||
TermSize PlusLevel Source # | |||||
GetDefs PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => PlusLevel -> m () Source # | |||||
TermLike PlusLevel Source # | |||||
AllMetas PlusLevel Source # | |||||
NamesIn PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
KillRange PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal | |||||
AbsTerm PlusLevel Source # | |||||
EqualSy PlusLevel Source # | |||||
CheckInternal PlusLevel Source # | |||||
Defined in Agda.TypeChecking.CheckInternal checkInternal' :: MonadCheckInternal m => Action m -> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel Source # checkInternal :: MonadCheckInternal m => PlusLevel -> Comparison -> TypeOf PlusLevel -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => Action m -> PlusLevel -> m PlusLevel Source # inferInternal :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => PlusLevel -> m () Source # | |||||
PrecomputeFreeVars PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: PlusLevel -> FV PlusLevel Source # | |||||
ForceNotFree PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel | |||||
UsableRelevance PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> PlusLevel -> m Bool Source # | |||||
MentionsMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool Source # | |||||
AnyRigid PlusLevel Source # | |||||
Occurs PlusLevel Source # | |||||
IsInstantiatedMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars isInstantiatedMeta :: (MonadFail m, ReadTCState m) => PlusLevel -> m Bool Source # | |||||
UnFreezeMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => PlusLevel -> m () Source # | |||||
ComputeOccurrences PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Positivity | |||||
InstantiateFull PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Reduce PlusLevel Source # | |||||
Simplify PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj PlusLevel Source # | |||||
DeBruijn PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn deBruijnVar :: Int -> PlusLevel Source # debruijnNamedVar :: String -> Int -> PlusLevel Source # deBruijnView :: PlusLevel -> Maybe Int Source # | |||||
SynEq PlusLevel Source # | |||||
NFData PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Functor PlusLevel' Source # | |||||
Defined in Agda.Syntax.Internal fmap :: (a -> b) -> PlusLevel' a -> PlusLevel' b (<$) :: a -> PlusLevel' b -> PlusLevel' a # | |||||
Foldable PlusLevel' Source # | |||||
Defined in Agda.Syntax.Internal fold :: Monoid m => PlusLevel' m -> m foldMap :: Monoid m => (a -> m) -> PlusLevel' a -> m foldMap' :: Monoid m => (a -> m) -> PlusLevel' a -> m foldr :: (a -> b -> b) -> b -> PlusLevel' a -> b foldr' :: (a -> b -> b) -> b -> PlusLevel' a -> b foldl :: (b -> a -> b) -> b -> PlusLevel' a -> b foldl' :: (b -> a -> b) -> b -> PlusLevel' a -> b foldr1 :: (a -> a -> a) -> PlusLevel' a -> a foldl1 :: (a -> a -> a) -> PlusLevel' a -> a toList :: PlusLevel' a -> [a] null :: PlusLevel' a -> Bool length :: PlusLevel' a -> Int elem :: Eq a => a -> PlusLevel' a -> Bool maximum :: Ord a => PlusLevel' a -> a minimum :: Ord a => PlusLevel' a -> a sum :: Num a => PlusLevel' a -> a product :: Num a => PlusLevel' a -> a | |||||
Traversable PlusLevel' Source # | |||||
Defined in Agda.Syntax.Internal traverse :: Applicative f => (a -> f b) -> PlusLevel' a -> f (PlusLevel' b) sequenceA :: Applicative f => PlusLevel' (f a) -> f (PlusLevel' a) mapM :: Monad m => (a -> m b) -> PlusLevel' a -> m (PlusLevel' b) sequence :: Monad m => PlusLevel' (m a) -> m (PlusLevel' a) | |||||
Eq PlusLevel | |||||
Ord PlusLevel | |||||
Defined in Agda.TypeChecking.Substitute | |||||
Free t => Free (PlusLevel' t) Source # | |||||
Defined in Agda.TypeChecking.Free.Lazy | |||||
Instantiate t => Instantiate (PlusLevel' t) Source # | |||||
Defined in Agda.TypeChecking.Reduce instantiate' :: PlusLevel' t -> ReduceM (PlusLevel' t) Source # | |||||
IsMeta a => IsMeta (PlusLevel' a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Subst a => Subst (PlusLevel' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute
applySubst :: Substitution' (SubstArg (PlusLevel' a)) -> PlusLevel' a -> PlusLevel' a Source # | |||||
Show t => Show (PlusLevel' t) Source # | |||||
Defined in Agda.Syntax.Internal showsPrec :: Int -> PlusLevel' t -> ShowS show :: PlusLevel' t -> String showList :: [PlusLevel' t] -> ShowS | |||||
type TypeOf PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type TypeOf [PlusLevel] Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type SubstArg (PlusLevel' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute |
Patterns are variables, constructors, or wildcards.
QName
is used in ConP
rather than Name
since
a constructor might come from a particular namespace.
This also meshes well with the fact that values (i.e.
the arguments we are matching with) use QName
.
VarP PatternInfo x | x |
DotP PatternInfo Term | .t |
ConP ConHead ConPatternInfo [NamedArg (Pattern' x)] |
|
LitP PatternInfo Literal | E.g. |
ProjP ProjOrigin QName | Projection copattern. Can only appear by itself. |
IApplyP PatternInfo Term Term x | Path elimination pattern, like |
DefP PatternInfo QName [NamedArg (Pattern' x)] | Used for HITs, the QName should be the one from primHComp. |
Instances
UsableSizeVars DeBruijnPattern Source # | |||||
Defined in Agda.Termination.Monad | |||||
UsableSizeVars MaskedDeBruijnPatterns Source # | |||||
Defined in Agda.Termination.Monad | |||||
Reduce DeBruijnPattern Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Subst DeBruijnPattern Source # | |||||
Defined in Agda.TypeChecking.Substitute
| |||||
Subst Pattern Source # | |||||
Defined in Agda.TypeChecking.Substitute applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern Source # | |||||
Subst SplitPattern Source # | |||||
Defined in Agda.TypeChecking.Coverage.Match
| |||||
Functor Pattern' Source # | |||||
Foldable Pattern' Source # | |||||
Defined in Agda.Syntax.Internal fold :: Monoid m => Pattern' m -> m foldMap :: Monoid m => (a -> m) -> Pattern' a -> m foldMap' :: Monoid m => (a -> m) -> Pattern' a -> m foldr :: (a -> b -> b) -> b -> Pattern' a -> b foldr' :: (a -> b -> b) -> b -> Pattern' a -> b foldl :: (b -> a -> b) -> b -> Pattern' a -> b foldl' :: (b -> a -> b) -> b -> Pattern' a -> b foldr1 :: (a -> a -> a) -> Pattern' a -> a foldl1 :: (a -> a -> a) -> Pattern' a -> a elem :: Eq a => a -> Pattern' a -> Bool maximum :: Ord a => Pattern' a -> a minimum :: Ord a => Pattern' a -> a | |||||
Traversable Pattern' Source # | |||||
LabelPatVars Pattern DeBruijnPattern Source # | |||||
Defined in Agda.Syntax.Internal.Pattern
labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern Source # | |||||
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
PatternLike a (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Internal | |||||
IsProjP (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Internal isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |||||
Pretty a => Pretty (Pattern' a) Source # | |||||
PatternVars (Arg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal
patternVars :: Arg (Pattern' a) -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)] Source # | |||||
PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal
patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source # | |||||
NamesIn (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
CountPatternVars (Pattern' x) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern countPatternVars :: Pattern' x -> Int Source # | |||||
PatternVarModalities (Pattern' x) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern
| |||||
KillRange a => KillRange (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Internal killRange :: KillRangeT (Pattern' a) Source # | |||||
UsableSizeVars (Masked DeBruijnPattern) Source # | |||||
Defined in Agda.Termination.Monad | |||||
UsableSizeVars [DeBruijnPattern] Source # | |||||
Defined in Agda.Termination.Monad usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source # | |||||
PrettyTCM a => PrettyTCM (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
NormaliseProjP (Pattern' x) Source # | |||||
Defined in Agda.TypeChecking.Records normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x) Source # | |||||
InstantiateFull a => InstantiateFull (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise a => Normalise (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
IsFlexiblePattern (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern' a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern' a -> m Bool Source # | |||||
EmbPrj a => EmbPrj (Pattern' a) Source # | |||||
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
DeBruijn a => DeBruijn (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute deBruijnVar :: Int -> Pattern' a Source # debruijnNamedVar :: String -> Int -> Pattern' a Source # deBruijnView :: Pattern' a -> Maybe Int Source # | |||||
DeBruijn a => IApplyVars (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path iApplyVars :: Pattern' a -> [Int] Source # | |||||
NFData x => NFData (Pattern' x) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Generic (Pattern' x) Source # | |||||
Defined in Agda.Syntax.Internal
| |||||
Show x => Show (Pattern' x) Source # | |||||
Eq a => Eq (Pattern' a) | |||||
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
type PatVarLabel DeBruijnPattern Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
type SubstArg DeBruijnPattern Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type SubstArg Pattern Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type SubstArg SplitPattern Source # | |||||
Defined in Agda.TypeChecking.Coverage.Match | |||||
type PatternVarOut (Arg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type PatVar (Pattern' x) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
type Rep (Pattern' x) Source # | |||||
Defined in Agda.Syntax.Internal type Rep (Pattern' x) = D1 ('MetaData "Pattern'" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 x)) :+: (C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConHead) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' x)]))))) :+: ((C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "IApplyP" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 x))) :+: C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' x)])))))) |
class TermSize a where Source #
The size of a term is roughly the number of nodes in its syntax tree. This number need not be precise for logical correctness of Agda, it is only used for reporting (and maybe decisions regarding performance).
Not counting towards the term size are:
- sort and color annotations,
- projections.
Instances
TermSize Level Source # | |
TermSize PlusLevel Source # | |
TermSize Sort Source # | |
TermSize Term Source # | |
TermSize a => TermSize (Substitution' a) Source # | |
Defined in Agda.Syntax.Internal termSize :: Substitution' a -> Int Source # tsize :: Substitution' a -> Sum Int Source # | |
(Foldable t, TermSize a) => TermSize (t a) Source # | |
type NotBlocked = NotBlocked' Term Source #
argFromDom :: Dom' t a -> Arg a Source #
namedArgFromDom :: Dom' t a -> NamedArg a Source #
domFromArg :: Arg a -> Dom a Source #
domFromNamedArg :: NamedArg a -> Dom a Source #
defaultDom :: a -> Dom a Source #
defaultArgDom :: ArgInfo -> a -> Dom a Source #
defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a Source #
data DataOrRecord' p Source #
Instances
CopatternMatchingAllowed DataOrRecord Source # | |||||
Defined in Agda.Syntax.Internal copatternMatchingAllowed :: DataOrRecord -> Bool Source # | |||||
PatternMatchingAllowed DataOrRecord Source # | |||||
Defined in Agda.Syntax.Internal patternMatchingAllowed :: DataOrRecord -> Bool Source # | |||||
KillRange DataOrRecord Source # | |||||
Defined in Agda.Syntax.Internal | |||||
EmbPrj DataOrRecord Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Internal icode :: DataOrRecord -> S Int32 Source # icod_ :: DataOrRecord -> S Int32 Source # value :: Int32 -> R DataOrRecord Source # | |||||
NFData DataOrRecord Source # | |||||
Defined in Agda.Syntax.Internal rnf :: DataOrRecord -> () | |||||
NFData DataOrRecordE | |||||
Defined in Agda.TypeChecking.Monad.Base rnf :: DataOrRecordE -> () | |||||
Generic (DataOrRecord' p) Source # | |||||
Defined in Agda.Syntax.Internal
from :: DataOrRecord' p -> Rep (DataOrRecord' p) x to :: Rep (DataOrRecord' p) x -> DataOrRecord' p | |||||
Show p => Show (DataOrRecord' p) Source # | |||||
Defined in Agda.Syntax.Internal showsPrec :: Int -> DataOrRecord' p -> ShowS show :: DataOrRecord' p -> String showList :: [DataOrRecord' p] -> ShowS | |||||
Eq p => Eq (DataOrRecord' p) Source # | |||||
Defined in Agda.Syntax.Internal (==) :: DataOrRecord' p -> DataOrRecord' p -> Bool (/=) :: DataOrRecord' p -> DataOrRecord' p -> Bool | |||||
type Rep (DataOrRecord' p) Source # | |||||
Defined in Agda.Syntax.Internal type Rep (DataOrRecord' p) = D1 ('MetaData "DataOrRecord'" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "IsData" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p))) |
class LensConName a where Source #
getConName :: a -> QName Source #
setConName :: QName -> a -> a Source #
mapConName :: (QName -> QName) -> a -> a Source #
Instances
LensConName ConHead Source # | |
Defined in Agda.Syntax.Internal |
Types are terms with a sort annotation.
Instances
Pretty Type Source # | |||||
TelToArgs ListTel Source # | |||||
TelToArgs Telescope Source # | |||||
GetDefs Telescope Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Telescope -> m () Source # | |||||
GetDefs Type Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Type -> m () Source # | |||||
TermLike Type Source # | |||||
AllMetas Type Source # | |||||
Reify Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract
| |||||
Reify Type Source # | |||||
TerSetSizeDepth ListTel Source # | |||||
Defined in Agda.Termination.Monad | |||||
TerSetSizeDepth Telescope Source # | |||||
Defined in Agda.Termination.Monad | |||||
AbsTerm Type Source # | |||||
EqualSy Type Source # | Ignores sorts. | ||||
CheckInternal Type Source # | |||||
Defined in Agda.TypeChecking.CheckInternal checkInternal' :: MonadCheckInternal m => Action m -> Type -> Comparison -> TypeOf Type -> m Type Source # checkInternal :: MonadCheckInternal m => Type -> Comparison -> TypeOf Type -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Type ~ ()) => Action m -> Type -> m Type Source # inferInternal :: (MonadCheckInternal m, TypeOf Type ~ ()) => Type -> m () Source # | |||||
DropArgs Telescope Source # | NOTE: This creates telescopes with unbound de Bruijn indices. | ||||
PrecomputeFreeVars Type Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute precomputeFreeVars :: Type -> FV Type Source # | |||||
ForceNotFree Type Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce forceNotFree' :: MonadFreeRed m => Type -> m Type | |||||
MentionsMeta Type Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Type -> Bool Source # | |||||
AnyRigid Type Source # | |||||
Occurs Type Source # | |||||
AddContext Telescope Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => Telescope -> m a -> m a Source # contextSize :: Telescope -> Nat Source # | |||||
UnFreezeMeta Type Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => Type -> m () Source # | |||||
ComputeOccurrences Type Source # | |||||
Defined in Agda.TypeChecking.Positivity occurrences :: Type -> OccM OccurrencesBuilder Source # | |||||
PrettyTCM Telescope Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM Type Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM ContextEntry Source # | |||||
Defined in Agda.TypeChecking.Pretty prettyTCM :: MonadPretty m => ContextEntry -> m Doc Source # | |||||
PrimTerm Type Source # | |||||
PrimType Type Source # | |||||
ToTerm Type Source # | |||||
Reduce Telescope Source # | |||||
Reduce Type Source # | |||||
TeleNoAbs ListTel Source # | |||||
TeleNoAbs Telescope Source # | |||||
Abstract Telescope Source # | |||||
Abstract Type Source # | |||||
SynEq Type Source # | Syntactic equality ignores sorts. | ||||
NFData Type Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Match NLPType Type Source # | |||||
NLPatToTerm NLPType Type Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
PatternFrom Type NLPType Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
LensSort (Type' a) Source # | |||||
SgTel (Dom Type) Source # | |||||
SgTel (Dom (ArgName, Type)) Source # | |||||
NamesIn a => NamesIn (Type' a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
KillRange a => KillRange (Type' a) Source # | |||||
Defined in Agda.Syntax.Internal killRange :: KillRangeT (Type' a) Source # | |||||
Free t => Free (Type' t) Source # | |||||
UsableRelevance a => UsableModality (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Type' a -> m Bool Source # | |||||
UsableRelevance a => UsableRelevance (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Type' a -> m Bool Source # | |||||
Occurs (Abs Type) Source # | |||||
AddContext (Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => Dom Type -> m a -> m a Source # | |||||
AddContext (Dom (Name, Type)) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source # | |||||
AddContext (Dom (String, Type)) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source # | |||||
AddContext (KeepNames Telescope) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # | |||||
IsSizeType a => IsSizeType (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Monad.SizedTypes isSizeType :: (HasOptions m, HasBuiltins m) => Type' a -> m (Maybe BoundedSize) Source # | |||||
PrettyTCM (Arg Type) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM (Type' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
ToTerm (Dom Type) Source # | |||||
Instantiate t => Instantiate (Type' t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull t => InstantiateFull (Type' t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise t => Normalise (Type' t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Simplify t => Simplify (Type' t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj a => EmbPrj (Type' a) Source # | |||||
Decoration (Type'' t) Source # | |||||
Functor (Type'' t) Source # | |||||
Foldable (Type'' t) Source # | |||||
Defined in Agda.Syntax.Internal fold :: Monoid m => Type'' t m -> m foldMap :: Monoid m => (a -> m) -> Type'' t a -> m foldMap' :: Monoid m => (a -> m) -> Type'' t a -> m foldr :: (a -> b -> b) -> b -> Type'' t a -> b foldr' :: (a -> b -> b) -> b -> Type'' t a -> b foldl :: (b -> a -> b) -> b -> Type'' t a -> b foldl' :: (b -> a -> b) -> b -> Type'' t a -> b foldr1 :: (a -> a -> a) -> Type'' t a -> a foldl1 :: (a -> a -> a) -> Type'' t a -> a elem :: Eq a => a -> Type'' t a -> Bool maximum :: Ord a => Type'' t a -> a minimum :: Ord a => Type'' t a -> a | |||||
Traversable (Type'' t) Source # | |||||
Eq a => Eq (Type' a) | Syntactic | ||||
Ord a => Ord (Type' a) | |||||
SgTel (ArgName, Dom Type) Source # | |||||
AddContext (Name, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source # | |||||
AddContext (KeepNames String, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a Source # | |||||
AddContext (List1 Name, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext (List1 (Arg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext (List1 (WithHiding Name), Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat Source # | |||||
AddContext (Text, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source # | |||||
AddContext (String, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source # | |||||
AddContext ([Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source # | |||||
AddContext ([Arg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # | |||||
AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
AddContext ([WithHiding Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source # | |||||
IsMeta a => IsMeta (Type'' t a) Source # | |||||
(Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) Source # | |||||
Defined in Agda.TypeChecking.Substitute
applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b Source # | |||||
(Show t, Show a) => Show (Type'' t a) Source # | |||||
type TypeOf Type Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type ReifiesTo Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type ReifiesTo Type Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type TypeOf (Abs Type) Source # | |||||
type SubstArg (Type'' a b) Source # | |||||
Defined in Agda.TypeChecking.Substitute |
Sequence of types. An argument of the first type is bound in later types and so on.
Instances
TelToArgs Telescope Source # | |||||
GetDefs Telescope Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => Telescope -> m () Source # | |||||
Reify Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract
| |||||
TerSetSizeDepth Telescope Source # | |||||
Defined in Agda.Termination.Monad | |||||
DropArgs Telescope Source # | NOTE: This creates telescopes with unbound de Bruijn indices. | ||||
AddContext Telescope Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => Telescope -> m a -> m a Source # contextSize :: Telescope -> Nat Source # | |||||
PrettyTCM Telescope Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
Reduce Telescope Source # | |||||
TeleNoAbs Telescope Source # | |||||
Abstract Telescope Source # | |||||
Functor Tele Source # | |||||
Foldable Tele Source # | |||||
Defined in Agda.Syntax.Internal fold :: Monoid m => Tele m -> m foldMap :: Monoid m => (a -> m) -> Tele a -> m foldMap' :: Monoid m => (a -> m) -> Tele a -> m foldr :: (a -> b -> b) -> b -> Tele a -> b foldr' :: (a -> b -> b) -> b -> Tele a -> b foldl :: (b -> a -> b) -> b -> Tele a -> b foldl' :: (b -> a -> b) -> b -> Tele a -> b foldr1 :: (a -> a -> a) -> Tele a -> a foldl1 :: (a -> a -> a) -> Tele a -> a elem :: Eq a => a -> Tele a -> Bool maximum :: Ord a => Tele a -> a | |||||
Traversable Tele Source # | |||||
Pretty a => Pretty (Tele (Dom a)) Source # | |||||
TermLike a => TermLike (Tele a) Source # | |||||
TermLike a => AllMetas (Tele a) Source # | |||||
NamesIn a => NamesIn (Tele a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
KillRange a => KillRange (Tele a) Source # | |||||
Defined in Agda.Syntax.Internal killRange :: KillRangeT (Tele a) Source # | |||||
Free t => Free (Tele t) Source # | |||||
MentionsMeta a => MentionsMeta (Tele a) Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention mentionsMetas :: HashSet MetaId -> Tele a -> Bool Source # | |||||
AddContext (KeepNames Telescope) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # | |||||
ComputeOccurrences a => ComputeOccurrences (Tele a) Source # | |||||
Defined in Agda.TypeChecking.Positivity occurrences :: Tele a -> OccM OccurrencesBuilder Source # | |||||
Instantiate t => Instantiate (Tele t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
(Subst a, Normalise a) => Normalise (Tele a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
(Subst a, Simplify a) => Simplify (Tele a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj a => EmbPrj (Tele a) Source # | |||||
TermSubst a => Apply (Tele a) Source # | |||||
Subst a => Subst (Tele a) Source # | |||||
Defined in Agda.TypeChecking.Substitute applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a Source # | |||||
Null (Tele a) Source # | |||||
Sized (Tele a) Source # | The size of a telescope is its length (as a list). | ||||
NFData a => NFData (Tele a) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Generic (Tele a) Source # | |||||
Defined in Agda.Syntax.Internal
| |||||
Show a => Show (Tele a) Source # | |||||
(Subst a, Eq a) => Eq (Tele a) | |||||
(Subst a, Ord a) => Ord (Tele a) | |||||
type ReifiesTo Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type SubstArg (Tele a) Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type Rep (Tele a) Source # | |||||
Defined in Agda.Syntax.Internal type Rep (Tele a) = D1 ('MetaData "Tele" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "EmptyTel" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExtendTel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Abs (Tele a))))) |
isStrictDataSort :: Sort' t -> Bool Source #
Is this a strict universe inhabitable by data types?
type PlusLevel = PlusLevel' Term Source #
Newtypes for terms that produce a dummy, rather than crash, when applied to incompatible eliminations.
Instances
Apply BraveTerm Source # | |
Subst BraveTerm Source # | |
Defined in Agda.TypeChecking.Substitute applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source # | |
DeBruijn BraveTerm Source # | |
Defined in Agda.TypeChecking.Substitute deBruijnVar :: Int -> BraveTerm Source # debruijnNamedVar :: String -> Int -> BraveTerm Source # deBruijnView :: BraveTerm -> Maybe Int Source # | |
Show BraveTerm Source # | |
type SubstArg BraveTerm Source # | |
Defined in Agda.TypeChecking.Substitute |
type NAPs = [NamedArg DeBruijnPattern] Source #
Named pattern arguments.
type DeBruijnPattern = Pattern' DBPatVar Source #
clausePats :: Clause -> [Arg DeBruijnPattern] Source #
type PatVarName = ArgName Source #
Pattern variables.
patVarNameToString :: PatVarName -> String Source #
nameToPatVarName :: Name -> PatVarName Source #
data PatternInfo Source #
PatternInfo | |
|
Instances
KillRange PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal | |||||
EmbPrj PatternInfo Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Internal icode :: PatternInfo -> S Int32 Source # icod_ :: PatternInfo -> S Int32 Source # value :: Int32 -> R PatternInfo Source # | |||||
NFData PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal rnf :: PatternInfo -> () | |||||
Generic PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal
from :: PatternInfo -> Rep PatternInfo x to :: Rep PatternInfo x -> PatternInfo | |||||
Show PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal showsPrec :: Int -> PatternInfo -> ShowS show :: PatternInfo -> String showList :: [PatternInfo] -> ShowS | |||||
Eq PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal (==) :: PatternInfo -> PatternInfo -> Bool (/=) :: PatternInfo -> PatternInfo -> Bool | |||||
type Rep PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal type Rep PatternInfo = D1 ('MetaData "PatternInfo" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "PatternInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "patOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatOrigin) :*: S1 ('MetaSel ('Just "patAsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))) |
Origin of the pattern: what did the user write in this position?
PatOSystem | Pattern inserted by the system |
PatOSplit | Pattern generated by case split |
PatOVar Name | User wrote a variable pattern |
PatODot | User wrote a dot pattern |
PatOWild | User wrote a wildcard pattern |
PatOCon | User wrote a constructor pattern |
PatORec | User wrote a record pattern |
PatOLit | User wrote a literal pattern |
PatOAbsurd | User wrote an absurd pattern |
Instances
KillRange PatOrigin Source # | |||||
Defined in Agda.Syntax.Internal | |||||
EmbPrj PatOrigin Source # | |||||
NFData PatOrigin Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Generic PatOrigin Source # | |||||
Defined in Agda.Syntax.Internal
| |||||
Show PatOrigin Source # | |||||
Eq PatOrigin Source # | |||||
type Rep PatOrigin Source # | |||||
Defined in Agda.Syntax.Internal type Rep PatOrigin = D1 ('MetaData "PatOrigin" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) (((C1 ('MetaCons "PatOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOSplit" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatOVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "PatODot" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatOWild" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PatOLit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOAbsurd" 'PrefixI 'False) (U1 :: Type -> Type))))) |
data ConPatternInfo Source #
The ConPatternInfo
states whether the constructor belongs to
a record type (True
) or data type (False
).
In the former case, the PatOrigin
of the conPInfo
says
whether the record pattern orginates from the expansion of an
implicit pattern.
The Type
is the type of the whole record pattern.
The scope used for the type is given by any outer scope
plus the clause's telescope (clauseTel
).
ConPatternInfo | |
|
Instances
NamesIn ConPatternInfo Source # | |||||
Defined in Agda.Syntax.Internal.Names namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> ConPatternInfo -> m Source # | |||||
KillRange ConPatternInfo Source # | |||||
Defined in Agda.Syntax.Internal | |||||
InstantiateFull ConPatternInfo Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise ConPatternInfo Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj ConPatternInfo Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Internal icode :: ConPatternInfo -> S Int32 Source # icod_ :: ConPatternInfo -> S Int32 Source # value :: Int32 -> R ConPatternInfo Source # | |||||
Subst ConPatternInfo Source # | |||||
Defined in Agda.TypeChecking.Substitute
| |||||
NFData ConPatternInfo Source # | |||||
Defined in Agda.Syntax.Internal rnf :: ConPatternInfo -> () | |||||
Generic ConPatternInfo Source # | |||||
Defined in Agda.Syntax.Internal
from :: ConPatternInfo -> Rep ConPatternInfo x to :: Rep ConPatternInfo x -> ConPatternInfo | |||||
Show ConPatternInfo Source # | |||||
Defined in Agda.Syntax.Internal showsPrec :: Int -> ConPatternInfo -> ShowS show :: ConPatternInfo -> String showList :: [ConPatternInfo] -> ShowS | |||||
type SubstArg ConPatternInfo Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type Rep ConPatternInfo Source # | |||||
Defined in Agda.Syntax.Internal type Rep ConPatternInfo = D1 ('MetaData "ConPatternInfo" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ConPatternInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conPInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Just "conPRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "conPFallThrough") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conPType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: S1 ('MetaSel ('Just "conPLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) |
Type used when numbering pattern variables.
DBPatVar | |
|
Instances
Pretty DBPatVar Source # | |||||
KillRange DBPatVar Source # | |||||
Defined in Agda.Syntax.Internal | |||||
UsableSizeVars DeBruijnPattern Source # | |||||
Defined in Agda.Termination.Monad | |||||
UsableSizeVars MaskedDeBruijnPatterns Source # | |||||
Defined in Agda.Termination.Monad | |||||
PrettyTCM DBPatVar Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
InstantiateFull DBPatVar Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise DBPatVar Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Reduce DeBruijnPattern Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj DBPatVar Source # | |||||
Subst DeBruijnPattern Source # | |||||
Defined in Agda.TypeChecking.Substitute
| |||||
DeBruijn DBPatVar Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn deBruijnVar :: Int -> DBPatVar Source # debruijnNamedVar :: String -> Int -> DBPatVar Source # deBruijnView :: DBPatVar -> Maybe Int Source # | |||||
NFData DBPatVar Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Generic DBPatVar Source # | |||||
Defined in Agda.Syntax.Internal
| |||||
Show DBPatVar Source # | |||||
Eq DBPatVar Source # | |||||
LabelPatVars Pattern DeBruijnPattern Source # | |||||
Defined in Agda.Syntax.Internal.Pattern
labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern Source # | |||||
UsableSizeVars (Masked DeBruijnPattern) Source # | |||||
Defined in Agda.Termination.Monad | |||||
UsableSizeVars [DeBruijnPattern] Source # | |||||
Defined in Agda.Termination.Monad usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source # | |||||
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.Clause | |||||
type PatVarLabel DeBruijnPattern Source # | |||||
Defined in Agda.Syntax.Internal.Pattern | |||||
type SubstArg DeBruijnPattern Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type Rep DBPatVar Source # | |||||
Defined in Agda.Syntax.Internal type Rep DBPatVar = D1 ('MetaData "DBPatVar" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DBPatVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "dbPatVarName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatVarName) :*: S1 ('MetaSel ('Just "dbPatVarIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) |
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern Source #
absurdP :: Int -> DeBruijnPattern Source #
Make an absurd pattern with the given de Bruijn index.
toConPatternInfo :: ConInfo -> ConPatternInfo Source #
Build partial ConPatternInfo
from ConInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo Source #
Build ConInfo
from ConPatternInfo
.
type family PatternVarOut a Source #
Instances
type PatternVarOut (Arg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal | |
type PatternVarOut (NamedArg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal | |
type PatternVarOut [a] Source # | |
Defined in Agda.Syntax.Internal |
patternInfo :: Pattern' x -> Maybe PatternInfo Source #
Retrieve the PatternInfo from a pattern
properlyMatching :: Pattern' a -> Bool Source #
Does the pattern perform a match that could fail?
:: Bool | Should absurd patterns count as proper match? |
-> Bool | Should projection patterns count as proper match? |
-> Pattern' a | The pattern. |
-> Bool |
data EqualityView Source #
View type as equality type.
EqualityViewType EqualityTypeData | |
OtherType Type | reduced |
IdiomType Type | reduced |
Instances
TermLike EqualityView Source # | |||||
Defined in Agda.Syntax.Internal.Generic traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView Source # foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m Source # | |||||
Free EqualityView Source # | |||||
Defined in Agda.TypeChecking.Free.Lazy | |||||
EqualityUnview EqualityView Source # | |||||
Defined in Agda.TypeChecking.Monad.Builtin equalityUnview :: EqualityView -> Type Source # | |||||
PrettyTCM EqualityView Source # | |||||
Defined in Agda.TypeChecking.Pretty prettyTCM :: MonadPretty m => EqualityView -> m Doc Source # | |||||
Instantiate EqualityView Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull EqualityView Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Normalise EqualityView Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Reduce EqualityView Source # | |||||
Defined in Agda.TypeChecking.Reduce reduce' :: EqualityView -> ReduceM EqualityView Source # reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) Source # | |||||
Simplify EqualityView Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Subst EqualityView Source # | |||||
Defined in Agda.TypeChecking.Substitute
| |||||
type SubstArg EqualityView Source # | |||||
Defined in Agda.TypeChecking.Substitute |
data EqualityTypeData Source #
Instances
EqualityUnview EqualityTypeData Source # | |||||
Defined in Agda.TypeChecking.Monad.Builtin | |||||
Subst EqualityTypeData Source # | |||||
Defined in Agda.TypeChecking.Substitute
| |||||
type SubstArg EqualityTypeData Source # | |||||
Defined in Agda.TypeChecking.Substitute |
pattern EqualityType :: Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView Source #
eqtSort :: EqualityView -> Sort Source #
eqtName :: EqualityView -> QName Source #
eqtParams :: EqualityView -> Args Source #
isEqualityType :: EqualityView -> Bool Source #
View type as path type.
isPathType :: PathView -> Bool Source #
data IntervalView Source #
Instances
Show IntervalView Source # | |
Defined in Agda.Syntax.Internal showsPrec :: Int -> IntervalView -> ShowS show :: IntervalView -> String showList :: [IntervalView] -> ShowS |
isIOne :: IntervalView -> Bool Source #
absurdBody :: Abs Term Source #
Absurd lambdas are internally represented as identity with variable name "()".
isAbsurdBody :: Abs Term -> Bool Source #
isAbsurdPatternName :: PatVarName -> Bool Source #
type DummyTermKind = String Source #
dummyLocName :: CallStack -> String Source #
Construct a string representing the call-site that created the dummy thing.
dummyTermWith :: DummyTermKind -> CallStack -> Term Source #
Aux: A dummy term to constitute a dummy termlevelsort/type.
dummyLevel :: CallStack -> Level Source #
A dummy level to constitute a level/sort created at location. Note: use macro DUMMY_LEVEL !
atomicLevel :: t -> Level' t Source #
dummyTerm :: CallStack -> Term Source #
A dummy term created at location. Note: use macro DUMMY_TERM !
__DUMMY_TERM__ :: HasCallStack => Term Source #
__DUMMY_LEVEL__ :: HasCallStack => Level Source #
dummySort :: CallStack -> Sort Source #
A dummy sort created at location. Note: use macro DUMMY_SORT !
__DUMMY_SORT__ :: HasCallStack => Sort Source #
dummyType :: CallStack -> Type Source #
A dummy type created at location. Note: use macro DUMMY_TYPE !
__DUMMY_TYPE__ :: HasCallStack => Type Source #
dummyDom :: CallStack -> Dom Type Source #
Context entries without a type have this dummy type. Note: use macro DUMMY_DOM !
__DUMMY_DOM__ :: HasCallStack => Dom Type Source #
pattern ClosedLevel :: Integer -> Level Source #
Constant level n
impossibleTerm :: CallStack -> Term Source #
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) Source #
A traversal for the names in a telescope.
telFromList :: ListTel -> Telescope Source #
Convert a list telescope to a telescope.
Constructing a singleton telescope.
class Suggest a where Source #
Suggest a name if available (i.e. name is not "_")
suggestName :: a -> Maybe String Source #
Instances
Suggest Name Source # | |
Defined in Agda.Syntax.Internal suggestName :: Name -> Maybe String Source # | |
Suggest Term Source # | |
Defined in Agda.Syntax.Internal suggestName :: Term -> Maybe String Source # | |
Suggest String Source # | |
Defined in Agda.Syntax.Internal suggestName :: String -> Maybe String Source # | |
Suggest (Abs b) Source # | |
Defined in Agda.Syntax.Internal suggestName :: Abs b -> Maybe String Source # |
data Suggestion Source #
Suggest a => Suggestion a |
suggests :: [Suggestion] -> String Source #
unSpine' :: (ProjOrigin -> QName -> Bool) -> Term -> Term Source #
Convert Proj
projection eliminations
according to their ProjOrigin
into
Def
projection applications.
hasElims :: Term -> Maybe (Elims -> Term, Elims) Source #
A view distinguishing the neutrals Var
, Def
, and MetaV
which
can be projected.
Instances
type TypeOf Elims Source # | |
type TypeOf Level Source # | |
Defined in Agda.Syntax.Internal | |
type TypeOf PlusLevel Source # | |
Defined in Agda.Syntax.Internal | |
type TypeOf Sort Source # | |
Defined in Agda.Syntax.Internal | |
type TypeOf Term Source # | |
Defined in Agda.Syntax.Internal | |
type TypeOf Type Source # | |
Defined in Agda.Syntax.Internal | |
type TypeOf NLPat Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
type TypeOf (Arg a) Source # | |
Defined in Agda.Syntax.Internal | |
type TypeOf (Abs Term) Source # | |
type TypeOf (Abs Type) Source # | |
type TypeOf (Dom a) Source # | |
Defined in Agda.Syntax.Internal | |
type TypeOf [PlusLevel] Source # | |
Defined in Agda.Syntax.Internal | |
type TypeOf [Elim' NLPat] Source # | |
prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc Source #
module Agda.Syntax.Internal.Elim
module Agda.Syntax.Internal.Univ
module Agda.Syntax.Abstract.Name
Meta-variable identifiers use the same structure as NameId
s.
MetaId | |
|
Instances
EncodeTCM MetaId Source # | |||||
Pretty MetaId Source # | |||||
GetDefs MetaId Source # | |||||
Defined in Agda.Syntax.Internal.Defs getDefs :: MonadGetDefs m => MetaId -> m () Source # | |||||
NamesIn MetaId Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
Reify MetaId Source # | |||||
HasFresh MetaId Source # | |||||
IsInstantiatedMeta MetaId Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source # | |||||
UnFreezeMeta MetaId Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source # | |||||
PrettyTCM MetaId Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
FromTerm MetaId Source # | |||||
Defined in Agda.TypeChecking.Primitive | |||||
PrimTerm MetaId Source # | |||||
PrimType MetaId Source # | |||||
ToTerm MetaId Source # | |||||
EmbPrj MetaId Source # | |||||
Unquote MetaId Source # | |||||
NFData MetaId Source # | |||||
Defined in Agda.Syntax.Common | |||||
Enum MetaId Source # | |||||
Generic MetaId Source # | |||||
Defined in Agda.Syntax.Common
| |||||
Show MetaId Source # | The record selectors are not included in the resulting strings. | ||||
Eq MetaId Source # | |||||
Ord MetaId Source # | |||||
Hashable MetaId Source # | |||||
Defined in Agda.Syntax.Common hashWithSalt :: Int -> MetaId -> Int | |||||
ToJSON MetaId Source # | |||||
Defined in Agda.Interaction.JSONTop | |||||
Singleton MetaId MetaSet Source # | |||||
Singleton MetaId () Source # | |||||
Defined in Agda.TypeChecking.Free.Lazy | |||||
InstantiateFull (Judgement MetaId) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
type ReifiesTo MetaId Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type Rep MetaId Source # | |||||
Defined in Agda.Syntax.Common type Rep MetaId = D1 ('MetaData "MetaId" "Agda.Syntax.Common" "Agda-2.6.20240714-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))) |
A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.
Instances
EncodeTCM ProblemId Source # | |
Pretty ProblemId Source # | |
HasFresh ProblemId Source # | |
PrettyTCM ProblemId Source # | |
Defined in Agda.TypeChecking.Pretty | |
EmbPrj ProblemId Source # | |
NFData ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Enum ProblemId Source # | |
Num ProblemId Source # | |
Integral ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Real ProblemId Source # | |
Defined in Agda.Syntax.Common toRational :: ProblemId -> Rational | |
Show ProblemId Source # | |
Eq ProblemId Source # | |
Ord ProblemId Source # | |
Defined in Agda.Syntax.Common | |
ToJSON ProblemId Source # | |
Defined in Agda.Interaction.JSONTop | |
Monad m => MonadFresh ProblemId (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure fresh :: PureConversionT m ProblemId Source # |