Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Internal
Contents
Synopsis
- type Type = Type' Term
- pattern Type :: Level' t -> Sort' t
- data Level' t = Max !Integer [PlusLevel' t]
- data ConHead = ConHead {
- conName :: QName
- conDataRecord :: DataOrRecord
- conInductive :: Induction
- conFields :: [Arg QName]
- data Term
- litP :: Literal -> Pattern' a
- varP :: a -> Pattern' a
- data Substitution' a
- = IdS
- | EmptyS Impossible
- | a :# (Substitution' a)
- | Strengthen Impossible !Int (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- 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
- 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)]
- type Telescope = Tele (Dom Type)
- data Dom' t e = Dom {}
- type Pattern = Pattern' PatVarName
- type Level = Level' Term
- telToList :: Tele (Dom t) -> [Dom (ArgName, t)]
- type Substitution = Substitution' Term
- type Dom = Dom' Term
- 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
- type Args = [Arg Term]
- data Abs a
- class LensSort a where
- type Elims = [Elim]
- arity :: Type -> Nat
- pattern Prop :: Level' t -> Sort' t
- pattern SSet :: Level' t -> Sort' t
- var :: Nat -> Term
- data PlusLevel' t = Plus !Integer t
- type Blocked = Blocked' Term
- class TermSize a where
- dontCare :: Term -> 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
- dotP :: Term -> Pattern' a
- data DBPatVar = DBPatVar {}
- 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
- 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 -> 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
A level is a maximum expression of a closed level and 0..n
PlusLevel
expressions each of which is an atom plus a number.
Constructors
Max !Integer [PlusLevel' t] |
Instances
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.
Constructors
ConHead | |
Fields
|
Instances
CopatternMatchingAllowed ConHead Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
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 Methods | |||||
SetRange ConHead Source # | |||||
PrettyTCM ConHead Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
InstantiateFull ConHead Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
EmbPrj ConHead Source # | |||||
Generic ConHead Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
Show ConHead Source # | |||||
NFData ConHead Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Eq ConHead Source # | |||||
Ord ConHead Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type Rep ConHead Source # | |||||
Defined in Agda.Syntax.Internal type Rep ConHead = D1 ('MetaData "ConHead" "Agda.Syntax.Internal" "Agda-2.6.4.2-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])))) |
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.
Constructors
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 Methods pretty :: CompiledClauses -> Doc Source # prettyPrec :: Int -> CompiledClauses -> Doc Source # prettyList :: [CompiledClauses] -> Doc Source # | |||||
LensSort Sort Source # | |||||
Suggest Term Source # | |||||
Defined in Agda.Syntax.Internal | |||||
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 Methods getDefs :: MonadGetDefs m => Level -> m () Source # | |||||
GetDefs PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => PlusLevel -> m () Source # | |||||
GetDefs Sort Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Sort -> m () Source # | |||||
GetDefs Telescope Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Telescope -> m () Source # | |||||
GetDefs Term Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Term -> m () Source # | |||||
GetDefs Type Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods 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 Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CompiledClauses -> m Source # | |||||
KillRange Level Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
KillRange PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
KillRange Sort Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
KillRange Substitution Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
KillRange Term Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
KillRange CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.CompiledClause Methods | |||||
Reify Level Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
Reify Sort Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
Reify Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
Reify Term Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
Reify Type Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
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 Methods 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 Methods 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 Methods 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 Methods 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 Methods 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 Methods 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 Methods dropArgs :: Int -> CompiledClauses -> CompiledClauses Source # | |||||
Free Level Source # | |||||
Free Sort Source # | |||||
Free Term Source # | |||||
PrecomputeFreeVars Level Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Level -> FV Level Source # | |||||
PrecomputeFreeVars PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: PlusLevel -> FV PlusLevel Source # | |||||
PrecomputeFreeVars Sort Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Sort -> FV Sort Source # | |||||
PrecomputeFreeVars Term Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Term -> FV Term Source # | |||||
PrecomputeFreeVars Type Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type Source # | |||||
ForceNotFree Level Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Level -> m Level | |||||
ForceNotFree PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel | |||||
ForceNotFree Sort Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Sort -> m Sort | |||||
ForceNotFree Term Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Term -> m Term | |||||
ForceNotFree Type Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Type -> m Type | |||||
UsableModality Level Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods 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 Methods 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 Methods 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 Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Level -> m Bool Source # | |||||
UsableRelevance PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> PlusLevel -> m Bool Source # | |||||
UsableRelevance Sort Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Sort -> m Bool Source # | |||||
UsableRelevance Term Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Term -> m Bool Source # | |||||
NoProjectedVar Term Source # | |||||
Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Term -> Either ProjectedVar () Source # | |||||
ReduceAndEtaContract Term Source # | |||||
Defined in Agda.TypeChecking.MetaVars | |||||
MentionsMeta Elim Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
MentionsMeta Level Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
MentionsMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
MentionsMeta Sort Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
MentionsMeta Term Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
MentionsMeta Type Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
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 Methods addContext :: MonadAddContext m => Telescope -> m a -> m a Source # contextSize :: Telescope -> Nat Source # | |||||
IsInstantiatedMeta Level Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Level -> m Bool Source # | |||||
IsInstantiatedMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => PlusLevel -> m Bool Source # | |||||
IsInstantiatedMeta Term Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Term -> m Bool Source # | |||||
UnFreezeMeta Level Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Level -> m () Source # | |||||
UnFreezeMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => PlusLevel -> m () Source # | |||||
UnFreezeMeta Sort Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source # | |||||
UnFreezeMeta Term Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Term -> m () Source # | |||||
UnFreezeMeta Type Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Type -> m () Source # | |||||
IsSizeType Term Source # | |||||
Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Term -> m (Maybe BoundedSize) Source # | |||||
ComputeOccurrences Level Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods | |||||
ComputeOccurrences PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods occurrences :: PlusLevel -> OccM OccurrencesBuilder Source # | |||||
ComputeOccurrences Term Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods occurrences :: Term -> OccM OccurrencesBuilder Source # | |||||
ComputeOccurrences Type Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods 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 Methods 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 Methods instantiateFull' :: Substitution -> ReduceM Substitution Source # | |||||
InstantiateFull Term Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses Source # | |||||
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 Methods getMatchables :: Term -> [QName] Source # | |||||
EmbPrj Blocked_ Source # | |||||
EmbPrj Level Source # | |||||
EmbPrj NotBlocked Source # | |||||
EmbPrj PlusLevel Source # | |||||
EmbPrj Sort Source # | |||||
EmbPrj Term Source # | |||||
EmbPrj 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 Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source # | |||||
Apply Sort Source # | |||||
Apply Term Source # | |||||
Apply CompiledClauses Source # | |||||
Defined in Agda.TypeChecking.Substitute Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source # | |||||
Subst Term Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg Term) -> Term -> Term Source # | |||||
DeBruijn Level Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn | |||||
DeBruijn PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn | |||||
DeBruijn Term Source # | We can substitute | ||||
Defined in Agda.TypeChecking.Substitute.DeBruijn | |||||
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 Methods piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> Term -> m Type Source # piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> Term -> m Type Source # | |||||
Show Term 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 | |||||
Eq Level Source # | |||||
Eq NotBlocked Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
Eq PlusLevel Source # | |||||
Eq Sort Source # | |||||
Eq Substitution Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
Eq Term Source # | Syntactic | ||||
Eq SingleLevel Source # | |||||
Defined in Agda.TypeChecking.Level | |||||
Ord Level Source # | |||||
Ord PlusLevel Source # | |||||
Ord Sort Source # | |||||
Ord Substitution Source # | |||||
Defined in Agda.TypeChecking.Substitute Methods 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 Source # | |||||
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 # | |||||
PatternFrom Sort NLPSort Source # | |||||
PatternFrom Term NLPat Source # | |||||
PatternFrom Type NLPType Source # | |||||
MonadError Blocked_ NLM Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |||||
Conversion TOM Term (MExp O) Source # | |||||
Conversion TOM Type (MExp O) Source # | |||||
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # | |||||
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Internal | |||||
PatternFrom Elims [Elim' NLPat] Source # | |||||
Conversion MOT (Exp O) Term Source # | |||||
Conversion MOT (Exp O) Type 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 Methods 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 Methods killRange :: KillRangeT (Blocked a) Source # | |||||
KillRange a => KillRange (Type' a) Source # | |||||
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Type' a) Source # | |||||
Reify i => Reify (Dom i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
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 Methods precomputeFreeVars :: Dom a -> FV (Dom a) Source # | |||||
(Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Dom a -> m (Dom a) | |||||
UsableModality a => UsableModality (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods 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 Methods 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 Methods 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 Methods 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 | |||||
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 Methods addContext :: MonadAddContext m => Dom Type -> m a -> m a Source # | |||||
AddContext (Dom (Name, Type)) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source # | |||||
AddContext (Dom (String, Type)) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source # | |||||
AddContext (KeepNames Telescope) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # | |||||
IsSizeType a => IsSizeType (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Dom a -> m (Maybe BoundedSize) Source # | |||||
IsSizeType a => IsSizeType (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Type' a -> m (Maybe BoundedSize) Source # | |||||
ComputeOccurrences a => ComputeOccurrences (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods 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 Methods 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 Associated Types
Methods 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) Source # | |||||
Eq a => Eq (Type' a) Source # | Syntactic | ||||
Ord a => Ord (Dom a) Source # | |||||
Ord a => Ord (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
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 # | |||||
SgTel (ArgName, Dom Type) Source # | |||||
(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types
Methods toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name)) Source # | |||||
AddContext (Name, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source # | |||||
AddContext (KeepNames String, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
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 Methods 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 Methods addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source # | |||||
AddContext (String, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source # | |||||
AddContext ([Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source # | |||||
AddContext ([Arg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # | |||||
AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
AddContext ([WithHiding Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source # | |||||
type 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 |
data Substitution' a Source #
Substitutions.
Constructors
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 Methods | |||||
InstantiateFull Substitution Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution Source # | |||||
Foldable Substitution' Source # | |||||
Defined in Agda.Syntax.Internal Methods 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 Methods 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) # | |||||
Functor Substitution' Source # | |||||
Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Substitution' a -> Substitution' b # (<$) :: a -> Substitution' b -> Substitution' a # | |||||
Eq Substitution Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
Ord Substitution Source # | |||||
Defined in Agda.TypeChecking.Substitute Methods 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 Methods 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 | |||||
NamesIn a => NamesIn (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal.Names Methods 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 Methods prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source # | |||||
EmbPrj a => EmbPrj (Substitution' a) Source # | |||||
EndoSubst a => Subst (Substitution' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source # | |||||
Null (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Generic (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
Methods 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 Methods showsPrec :: Int -> Substitution' a -> ShowS # show :: Substitution' a -> String # showList :: [Substitution' a] -> ShowS # | |||||
NFData a => NFData (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal Methods rnf :: Substitution' a -> () # | |||||
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.4.2-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)))))) |
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!
Constructors
Clause | |
Fields
|
Instances
Pretty Clause Source # | |||||
GetDefs Clause Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Clause -> m () Source # | |||||
NamesIn Clause Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
FunArity Clause Source # | Get the number of initial | ||||
HasRange Clause Source # | |||||
KillRange Clause Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
DropArgs Clause Source # | NOTE: does not work for recursive functions. | ||||
DropArgs FunctionInverse Source # | |||||
Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> FunctionInverse -> FunctionInverse Source # | |||||
Free Clause Source # | |||||
Occurs Clause Source # | |||||
ComputeOccurrences Clause Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods | |||||
PrettyTCM Clause Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
NormaliseProjP Clause Source # | |||||
Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Clause -> m Clause Source # | |||||
InstantiateFull Clause Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
InstantiateFull FunctionInverse Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse Source # | |||||
EmbPrj Clause Source # | |||||
Abstract Clause Source # | |||||
Abstract FunctionInverse Source # | |||||
Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse Source # | |||||
Apply Clause Source # | |||||
Apply FunctionInverse Source # | |||||
Defined in Agda.TypeChecking.Substitute Methods apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source # | |||||
Null Clause Source # | A | ||||
Generic Clause Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
Show Clause Source # | |||||
NFData Clause Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # | |||||
Conversion TOM [Clause] [([Pat O], MExp O)] Source # | |||||
FunArity [Clause] Source # | Get the number of common initial | ||||
Reify (QNamed Clause) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
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.4.2-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 |
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
.
Constructors
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 Methods | |||||
UsableSizeVars MaskedDeBruijnPatterns Source # | |||||
Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source # | |||||
Reduce DeBruijnPattern Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern Source # reduceB' :: DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern) Source # | |||||
Subst DeBruijnPattern Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source # | |||||
Subst Pattern Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern Source # | |||||
Subst SplitPattern Source # | |||||
Defined in Agda.TypeChecking.Coverage.Match Associated Types
Methods applySubst :: Substitution' (SubstArg SplitPattern) -> SplitPattern -> SplitPattern Source # | |||||
Foldable Pattern' Source # | |||||
Defined in Agda.Syntax.Internal Methods 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 # | |||||
Functor Pattern' Source # | |||||
LabelPatVars Pattern DeBruijnPattern Source # | |||||
Defined in Agda.Syntax.Internal.Pattern Associated Types
Methods labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern Source # | |||||
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
PatternLike a (Pattern' a) Source # | |||||
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Patterns.Internal | |||||
Conversion TOM (Arg Pattern) (Pat O) Source # | |||||
IsProjP (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |||||
Pretty a => Pretty (Pattern' a) Source # | |||||
PatternVars (Arg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
NamesIn (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
CountPatternVars (Pattern' x) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Pattern' x -> Int Source # | |||||
PatternVarModalities (Pattern' x) Source # | |||||
Defined in Agda.Syntax.Internal.Pattern Associated Types
| |||||
KillRange a => KillRange (Pattern' a) Source # | |||||
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Pattern' a) Source # | |||||
UsableSizeVars (Masked DeBruijnPattern) Source # | |||||
Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source # | |||||
UsableSizeVars [DeBruijnPattern] Source # | |||||
Defined in Agda.Termination.Monad Methods 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 Methods 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 Methods 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 | |||||
DeBruijn a => IApplyVars (Pattern' a) Source # | |||||
Defined in Agda.TypeChecking.Telescope.Path Methods iApplyVars :: Pattern' a -> [Int] Source # | |||||
Generic (Pattern' x) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
Show x => Show (Pattern' x) Source # | |||||
NFData x => NFData (Pattern' x) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Eq a => Eq (Pattern' a) 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 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.4.2-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)])))))) |
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.
Constructors
Dom | |
Instances
TelToArgs ListTel Source # | |||||
TelToArgs Telescope Source # | |||||
GetDefs Telescope Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Telescope -> m () Source # | |||||
Reify Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
TerSetSizeDepth ListTel Source # | |||||
Defined in Agda.Termination.Monad | |||||
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 Methods addContext :: MonadAddContext m => Telescope -> m a -> m a Source # contextSize :: Telescope -> Nat Source # | |||||
PrettyTCM Telescope Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
PrettyTCM ContextEntry Source # | |||||
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ContextEntry -> m Doc Source # | |||||
Reduce Telescope Source # | |||||
TeleNoAbs ListTel Source # | |||||
TeleNoAbs Telescope Source # | |||||
Abstract Telescope Source # | |||||
Pretty a => Pretty (Tele (Dom a)) Source # | |||||
LensSort a => LensSort (Dom a) Source # | |||||
SgTel (Dom Type) Source # | |||||
SgTel (Dom (ArgName, Type)) Source # | |||||
GetDefs a => GetDefs (Dom a) Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Dom a -> m () Source # | |||||
TermLike a => TermLike (Dom a) Source # | |||||
Reify i => Reify (Dom i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
AbsTerm a => AbsTerm (Dom a) Source # | |||||
EqualSy a => EqualSy (Dom a) Source # | Ignore the tactic. | ||||
Free t => Free (Dom t) Source # | |||||
PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Dom a -> FV (Dom a) Source # | |||||
(Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Dom a -> m (Dom a) | |||||
UsableModality a => UsableModality (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadError Blocker m) => Modality -> Dom a -> m Bool Source # | |||||
UsableRelevance a => UsableRelevance (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Dom a -> m Bool Source # | |||||
MentionsMeta t => MentionsMeta (Dom t) Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
AnyRigid a => AnyRigid (Dom a) Source # | |||||
Occurs a => Occurs (Dom a) Source # | |||||
AddContext (Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom Type -> m a -> m a Source # | |||||
AddContext (Dom (Name, Type)) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source # | |||||
AddContext (Dom (String, Type)) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source # | |||||
AddContext (KeepNames Telescope) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # | |||||
IsSizeType a => IsSizeType (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: (HasOptions m, HasBuiltins m) => Dom a -> m (Maybe BoundedSize) Source # | |||||
ComputeOccurrences a => ComputeOccurrences (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods occurrences :: Dom a -> OccM OccurrencesBuilder Source # | |||||
PrettyTCM (Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
ToTerm (Dom Type) Source # | |||||
Normalise t => Normalise (Dom t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Reduce t => Reduce (Dom t) Source # | |||||
Simplify t => Simplify (Dom t) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
GetMatchables a => GetMatchables (Dom a) Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Dom a -> [QName] Source # | |||||
EmbPrj a => EmbPrj (Dom a) Source # | |||||
SynEq a => SynEq (Dom a) Source # | |||||
Unquote a => Unquote (Dom a) Source # | |||||
Decoration (Dom' t) Source # | |||||
Foldable (Dom' t) Source # | |||||
Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Dom' t m -> m # foldMap :: Monoid m => (a -> m) -> Dom' t a -> m # foldMap' :: Monoid m => (a -> m) -> Dom' t a -> m # foldr :: (a -> b -> b) -> b -> Dom' t a -> b # foldr' :: (a -> b -> b) -> b -> Dom' t a -> b # foldl :: (b -> a -> b) -> b -> Dom' t a -> b # foldl' :: (b -> a -> b) -> b -> Dom' t a -> b # foldr1 :: (a -> a -> a) -> Dom' t a -> a # foldl1 :: (a -> a -> a) -> Dom' t a -> a # elem :: Eq a => a -> Dom' t a -> Bool # maximum :: Ord a => Dom' t a -> a # minimum :: Ord a => Dom' t a -> a # | |||||
Traversable (Dom' t) Source # | |||||
Functor (Dom' t) Source # | |||||
NFData e => NFData (Dom e) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Ord a => Ord (Dom a) 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 # | |||||
LensAnnotation (Dom' t e) Source # | |||||
Defined in Agda.Syntax.Internal Methods getAnnotation :: Dom' t e -> Annotation Source # setAnnotation :: Annotation -> Dom' t e -> Dom' t e Source # mapAnnotation :: (Annotation -> Annotation) -> Dom' t e -> Dom' t e Source # | |||||
LensArgInfo (Dom' t e) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
LensCohesion (Dom' t e) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
LensFreeVariables (Dom' t e) Source # | |||||
Defined in Agda.Syntax.Internal Methods getFreeVariables :: Dom' t e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Dom' t e -> Dom' t e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom' t e -> Dom' t e Source # | |||||
LensHiding (Dom' t e) Source # | |||||
LensLock (Dom' t e) Source # | |||||
LensModality (Dom' t e) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
LensNamed (Dom' t e) Source # | |||||
LensOrigin (Dom' t e) Source # | |||||
LensQuantity (Dom' t e) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
LensRelevance (Dom' t e) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
(Pretty t, Pretty e) => Pretty (Dom' t e) Source # | |||||
SgTel (ArgName, Dom Type) Source # | |||||
(AllMetas a, AllMetas b) => AllMetas (Dom' a b) Source # | |||||
(NamesIn a, NamesIn b) => NamesIn (Dom' a b) Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
HasRange a => HasRange (Dom' t a) Source # | |||||
(KillRange t, KillRange a) => KillRange (Dom' t a) Source # | |||||
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Dom' t a) Source # | |||||
(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types
Methods toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name)) Source # | |||||
AddContext (Name, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source # | |||||
AddContext (KeepNames String, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext (List1 Name, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
AddContext (List1 (WithHiding Name), Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # contextSize :: (List1 (WithHiding Name), Dom Type) -> Nat Source # | |||||
AddContext (Text, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source # | |||||
AddContext (String, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source # | |||||
AddContext ([Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source # | |||||
AddContext ([WithHiding Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source # | |||||
(Instantiate t, Instantiate e) => Instantiate (Dom' t e) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
(InstantiateFull t, InstantiateFull e) => InstantiateFull (Dom' t e) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Dom' a b)) -> Dom' a b -> Dom' a b Source # | |||||
(Show t, Show e) => Show (Dom' t e) Source # | |||||
Eq a => Eq (Dom' t a) Source # | Ignores | ||||
type ReifiesTo Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type TypeOf (Dom a) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type ReifiesTo (Dom i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract | |||||
type NameOf (Dom' t e) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type AbsOfRef (Dom r, Name) Source # | |||||
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |||||
type SubstArg (Dom' a b) Source # | |||||
Defined in Agda.TypeChecking.Substitute |
Arguments
= Pattern' PatVarName | The |
type Substitution = Substitution' Term Source #
Sorts.
Constructors
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 Methods 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 Methods | |||||
Reify Sort Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
AbsTerm Sort Source # | |||||
EqualSy Sort Source # | |||||
CheckInternal Sort Source # | |||||
Defined in Agda.TypeChecking.CheckInternal Methods 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 Methods precomputeFreeVars :: Sort -> FV Sort Source # | |||||
ForceNotFree Sort Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Sort -> m Sort | |||||
UsableModality Sort Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods 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 Methods 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 | |||||
AnyRigid Sort Source # | |||||
Occurs Sort Source # | |||||
UnFreezeMeta Sort Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods 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 Source # | |||||
Ord Sort Source # | |||||
Match NLPSort Sort Source # | |||||
NLPatToTerm NLPSort Sort Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |||||
PatternFrom Sort NLPSort Source # | |||||
IsMeta a => IsMeta (Sort' a) Source # | |||||
(Coercible a Term, Subst a) => Subst (Sort' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods 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
).
Associated Types
type PatternVarOut a Source #
Methods
patternVars :: a -> [Arg (Either (PatternVarOut a) Term)] Source #
Instances
PatternVars (Arg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
PatternVars a => PatternVars [a] Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
Methods patternVars :: [a] -> [Arg (Either (PatternVarOut [a]) Term)] Source # |
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.
Constructors
Abs | The body has (at least) one free variable.
Danger: |
NoAbs | |
Instances
Decoration Abs Source # | |||||
Foldable Abs Source # | |||||
Defined in Agda.Syntax.Internal Methods 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 # | |||||
Functor Abs Source # | |||||
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source # | |||||
Pretty t => Pretty (Abs t) Source # | |||||
Suggest (Abs b) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
GetDefs a => GetDefs (Abs a) Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods 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 Methods killRange :: KillRangeT (Abs a) Source # | |||||
(Free i, Reify i) => Reify (Abs i) Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
(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 Methods precomputeFreeVars :: Abs a -> FV (Abs a) Source # | |||||
(Reduce a, ForceNotFree a) => ForceNotFree (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Abs a -> m (Abs a) | |||||
(Subst a, UsableRelevance a) => UsableRelevance (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods 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 | |||||
(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 Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Abs a -> m Bool Source # | |||||
UnFreezeMeta a => UnFreezeMeta (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Abs a -> m () Source # | |||||
ComputeOccurrences a => ComputeOccurrences (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods 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 Methods getMatchables :: Abs a -> [QName] Source # | |||||
NLPatVars a => NLPatVars (Abs a) Source # | |||||
EmbPrj a => EmbPrj (Abs a) Source # | |||||
Subst a => Subst (Abs a) Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source # | |||||
(Subst a, SynEq a) => SynEq (Abs a) Source # | |||||
Sized a => Sized (Abs a) Source # | |||||
Generic (Abs a) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
Show a => Show (Abs a) Source # | |||||
NFData a => NFData (Abs a) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
(Subst a, Eq a) => Eq (Abs a) Source # | 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) Source # | |||||
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.4.2-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))) |
class LensSort a where Source #
Minimal complete definition
data PlusLevel' t Source #
Instances
Pretty PlusLevel Source # | |||||
TermSize PlusLevel Source # | |||||
GetDefs PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods 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 Methods | |||||
AbsTerm PlusLevel Source # | |||||
EqualSy PlusLevel Source # | |||||
CheckInternal PlusLevel Source # | |||||
Defined in Agda.TypeChecking.CheckInternal Methods 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 Methods precomputeFreeVars :: PlusLevel -> FV PlusLevel Source # | |||||
ForceNotFree PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel | |||||
UsableRelevance PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods 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 | |||||
AnyRigid PlusLevel Source # | |||||
Occurs PlusLevel Source # | |||||
IsInstantiatedMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => PlusLevel -> m Bool Source # | |||||
UnFreezeMeta PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => PlusLevel -> m () Source # | |||||
ComputeOccurrences PlusLevel Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods occurrences :: PlusLevel -> OccM OccurrencesBuilder Source # | |||||
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 | |||||
SynEq PlusLevel Source # | |||||
Foldable PlusLevel' Source # | |||||
Defined in Agda.Syntax.Internal Methods 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 Methods 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) # | |||||
Functor PlusLevel' Source # | |||||
Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> PlusLevel' a -> PlusLevel' b # (<$) :: a -> PlusLevel' b -> PlusLevel' a # | |||||
NFData PlusLevel Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Eq PlusLevel Source # | |||||
Ord PlusLevel Source # | |||||
Free t => Free (PlusLevel' t) Source # | |||||
Defined in Agda.TypeChecking.Free.Lazy | |||||
Instantiate t => Instantiate (PlusLevel' t) Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods 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 Associated Types
Methods applySubst :: Substitution' (SubstArg (PlusLevel' a)) -> PlusLevel' a -> PlusLevel' a Source # | |||||
Show t => Show (PlusLevel' t) Source # | |||||
Defined in Agda.Syntax.Internal Methods 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 |
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.
Minimal complete definition
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 #
data DataOrRecord' p Source #
Instances
CopatternMatchingAllowed DataOrRecord Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
PatternMatchingAllowed DataOrRecord Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
KillRange DataOrRecord Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
EmbPrj DataOrRecord Source # | |||||
NFData DataOrRecord Source # | |||||
Defined in Agda.Syntax.Internal Methods rnf :: DataOrRecord -> () # | |||||
NFData DataOrRecordE Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: DataOrRecordE -> () # | |||||
Generic (DataOrRecord' p) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
Methods 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 Methods showsPrec :: Int -> DataOrRecord' p -> ShowS # show :: DataOrRecord' p -> String # showList :: [DataOrRecord' p] -> ShowS # | |||||
Eq p => Eq (DataOrRecord' p) Source # | |||||
Defined in Agda.Syntax.Internal Methods (==) :: 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.4.2-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 #
Minimal complete definition
Methods
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 Methods getDefs :: MonadGetDefs m => Telescope -> m () Source # | |||||
GetDefs Type Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Type -> m () Source # | |||||
TermLike Type Source # | |||||
AllMetas Type Source # | |||||
Reify Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
Reify Type Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
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 Methods 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 Methods precomputeFreeVars :: Type -> FV Type Source # | |||||
ForceNotFree Type Source # | |||||
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Type -> m Type | |||||
MentionsMeta Type Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
AnyRigid Type Source # | |||||
Occurs Type Source # | |||||
AddContext Telescope Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Telescope -> m a -> m a Source # contextSize :: Telescope -> Nat Source # | |||||
UnFreezeMeta Type Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Type -> m () Source # | |||||
ComputeOccurrences Type Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods 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 Methods 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 # | |||||
Conversion TOM Type (MExp O) Source # | |||||
Conversion MOT (Exp O) Type Source # | |||||
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 Methods killRange :: KillRangeT (Type' a) Source # | |||||
Free t => Free (Type' t) Source # | |||||
UsableRelevance a => UsableModality (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Irrelevance Methods 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 Methods 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 Methods addContext :: MonadAddContext m => Dom Type -> m a -> m a Source # | |||||
AddContext (Dom (Name, Type)) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source # | |||||
AddContext (Dom (String, Type)) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source # | |||||
AddContext (KeepNames Telescope) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # | |||||
IsSizeType a => IsSizeType (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Monad.SizedTypes Methods 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 # | |||||
Foldable (Type'' t) Source # | |||||
Defined in Agda.Syntax.Internal Methods 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 # | |||||
Functor (Type'' t) Source # | |||||
Eq a => Eq (Type' a) Source # | Syntactic | ||||
Ord a => Ord (Type' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
SgTel (ArgName, Dom Type) Source # | |||||
AddContext (Name, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source # | |||||
AddContext (KeepNames String, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context | |||||
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 Methods 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 Methods addContext :: MonadAddContext m => (Text, Dom Type) -> m a -> m a Source # | |||||
AddContext (String, Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source # | |||||
AddContext ([Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source # | |||||
AddContext ([Arg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # | |||||
AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
AddContext ([WithHiding Name], Dom Type) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source # | |||||
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 Associated Types
Methods 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 Methods getDefs :: MonadGetDefs m => Telescope -> m () Source # | |||||
Reify Telescope Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
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 Methods 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 # | |||||
Foldable Tele Source # | |||||
Defined in Agda.Syntax.Internal Methods 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 # | |||||
Functor 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 Methods killRange :: KillRangeT (Tele a) Source # | |||||
Free t => Free (Tele t) Source # | |||||
MentionsMeta a => MentionsMeta (Tele a) Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
AddContext (KeepNames Telescope) Source # | |||||
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # | |||||
ComputeOccurrences a => ComputeOccurrences (Tele a) Source # | |||||
Defined in Agda.TypeChecking.Positivity Methods 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 Associated Types
Methods 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). | ||||
Generic (Tele a) Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
Show a => Show (Tele a) Source # | |||||
NFData a => NFData (Tele a) Source # | |||||
Defined in Agda.Syntax.Internal | |||||
(Subst a, Eq a) => Eq (Tele a) Source # | |||||
(Subst a, Ord a) => Ord (Tele a) Source # | |||||
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.4.2-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))))) |
Instances
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 Associated Types
Methods applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source # | |||||
DeBruijn BraveTerm Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
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.
nameToPatVarName :: Name -> PatVarName Source #
data PatternInfo Source #
Constructors
PatternInfo | |
Fields
|
Instances
KillRange PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
EmbPrj PatternInfo Source # | |||||
Generic PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
Show PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> PatternInfo -> ShowS # show :: PatternInfo -> String # showList :: [PatternInfo] -> ShowS # | |||||
NFData PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal Methods rnf :: PatternInfo -> () # | |||||
Eq PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal | |||||
type Rep PatternInfo Source # | |||||
Defined in Agda.Syntax.Internal type Rep PatternInfo = D1 ('MetaData "PatternInfo" "Agda.Syntax.Internal" "Agda-2.6.4.2-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?
Constructors
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 Methods | |||||
EmbPrj PatOrigin Source # | |||||
Generic PatOrigin Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
Show PatOrigin Source # | |||||
NFData PatOrigin Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Eq PatOrigin Source # | |||||
type Rep PatOrigin Source # | |||||
Defined in Agda.Syntax.Internal type Rep PatOrigin = D1 ('MetaData "PatOrigin" "Agda.Syntax.Internal" "Agda-2.6.4.2-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
).
Constructors
ConPatternInfo | |
Fields
|
Instances
KillRange ConPatternInfo Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
InstantiateFull ConPatternInfo Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo Source # | |||||
Normalise ConPatternInfo Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods normalise' :: ConPatternInfo -> ReduceM ConPatternInfo Source # | |||||
EmbPrj ConPatternInfo Source # | |||||
Subst ConPatternInfo Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg ConPatternInfo) -> ConPatternInfo -> ConPatternInfo Source # | |||||
Generic ConPatternInfo Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
Methods from :: ConPatternInfo -> Rep ConPatternInfo x # to :: Rep ConPatternInfo x -> ConPatternInfo # | |||||
Show ConPatternInfo Source # | |||||
Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> ConPatternInfo -> ShowS # show :: ConPatternInfo -> String # showList :: [ConPatternInfo] -> ShowS # | |||||
NFData ConPatternInfo Source # | |||||
Defined in Agda.Syntax.Internal Methods rnf :: ConPatternInfo -> () # | |||||
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.4.2-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.
Constructors
DBPatVar | |
Fields
|
Instances
Pretty DBPatVar Source # | |||||
KillRange DBPatVar Source # | |||||
Defined in Agda.Syntax.Internal Methods | |||||
UsableSizeVars DeBruijnPattern Source # | |||||
Defined in Agda.Termination.Monad Methods | |||||
UsableSizeVars MaskedDeBruijnPatterns Source # | |||||
Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source # | |||||
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 Methods reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern Source # reduceB' :: DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern) Source # | |||||
EmbPrj DBPatVar Source # | |||||
Subst DeBruijnPattern Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source # | |||||
DeBruijn DBPatVar Source # | |||||
Defined in Agda.TypeChecking.Substitute.DeBruijn | |||||
Generic DBPatVar Source # | |||||
Defined in Agda.Syntax.Internal Associated Types
| |||||
Show DBPatVar Source # | |||||
NFData DBPatVar Source # | |||||
Defined in Agda.Syntax.Internal | |||||
Eq DBPatVar Source # | |||||
LabelPatVars Pattern DeBruijnPattern Source # | |||||
Defined in Agda.Syntax.Internal.Pattern Associated Types
Methods labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern Source # | |||||
UsableSizeVars (Masked DeBruijnPattern) Source # | |||||
Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source # | |||||
UsableSizeVars [DeBruijnPattern] Source # | |||||
Defined in Agda.Termination.Monad Methods 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.4.2-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?
data EqualityView Source #
View type as equality type.
Constructors
EqualityViewType EqualityTypeData | |
OtherType Type | reduced |
IdiomType Type | reduced |
Instances
TermLike EqualityView Source # | |||||
Defined in Agda.Syntax.Internal.Generic Methods 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 Methods equalityUnview :: EqualityView -> Type Source # | |||||
PrettyTCM EqualityView Source # | |||||
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => EqualityView -> m Doc Source # | |||||
Instantiate EqualityView Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods instantiate' :: EqualityView -> ReduceM EqualityView Source # | |||||
InstantiateFull EqualityView Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: EqualityView -> ReduceM EqualityView Source # | |||||
Normalise EqualityView Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods | |||||
Reduce EqualityView Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods reduce' :: EqualityView -> ReduceM EqualityView Source # reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) Source # | |||||
Simplify EqualityView Source # | |||||
Defined in Agda.TypeChecking.Reduce Methods | |||||
Subst EqualityView Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg EqualityView) -> EqualityView -> EqualityView Source # | |||||
type SubstArg EqualityView Source # | |||||
Defined in Agda.TypeChecking.Substitute |
data EqualityTypeData Source #
Constructors
EqualityTypeData | |
Instances
EqualityUnview EqualityTypeData Source # | |||||
Defined in Agda.TypeChecking.Monad.Builtin Methods | |||||
Subst EqualityTypeData Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg EqualityTypeData) -> EqualityTypeData -> EqualityTypeData Source # | |||||
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 #
Constructors
IZero | |
IOne | |
IMin (Arg Term) (Arg Term) | |
IMax (Arg Term) (Arg Term) | |
INeg (Arg Term) | |
OTerm Term |
Instances
Show IntervalView Source # | |
Defined in Agda.Syntax.Internal Methods 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 "()".
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 "_")
Methods
suggestName :: a -> Maybe String Source #
Instances
Suggest Name Source # | |
Defined in Agda.Syntax.Internal | |
Suggest Term Source # | |
Defined in Agda.Syntax.Internal | |
Suggest String Source # | |
Defined in Agda.Syntax.Internal | |
Suggest (Abs b) Source # | |
Defined in Agda.Syntax.Internal |
data Suggestion Source #
Constructors
Suggest a => Suggestion a |
suggests :: [Suggestion] -> String Source #
unSpine' :: (ProjOrigin -> 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 # | |
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.
Constructors
MetaId | |
Fields
|
Instances
EncodeTCM MetaId Source # | |||||
Pretty MetaId Source # | |||||
GetDefs MetaId Source # | |||||
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => MetaId -> m () Source # | |||||
NamesIn MetaId Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
Reify MetaId Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types
| |||||
HasFresh MetaId Source # | |||||
IsInstantiatedMeta MetaId Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source # | |||||
UnFreezeMeta MetaId Source # | |||||
Defined in Agda.TypeChecking.Monad.MetaVars Methods 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 # | |||||
Enum MetaId Source # | |||||
Defined in Agda.Syntax.Common | |||||
Generic MetaId Source # | |||||
Defined in Agda.Syntax.Common Associated Types
| |||||
Show MetaId Source # | The record selectors are not included in the resulting strings. | ||||
NFData MetaId Source # | |||||
Defined in Agda.Syntax.Common | |||||
Eq MetaId Source # | |||||
Ord MetaId Source # | |||||
Hashable MetaId Source # | |||||
Defined in Agda.Syntax.Common | |||||
ToJSON MetaId Source # | |||||
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.4.2-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 | |
Enum ProblemId Source # | |
Defined in Agda.Syntax.Common Methods succ :: ProblemId -> ProblemId # pred :: ProblemId -> ProblemId # fromEnum :: ProblemId -> Int # enumFrom :: ProblemId -> [ProblemId] # enumFromThen :: ProblemId -> ProblemId -> [ProblemId] # enumFromTo :: ProblemId -> ProblemId -> [ProblemId] # enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId] # | |
Num ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Integral ProblemId Source # | |
Defined in Agda.Syntax.Common Methods quot :: ProblemId -> ProblemId -> ProblemId # rem :: ProblemId -> ProblemId -> ProblemId # div :: ProblemId -> ProblemId -> ProblemId # mod :: ProblemId -> ProblemId -> ProblemId # quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId) # divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId) # | |
Real ProblemId Source # | |
Defined in Agda.Syntax.Common Methods toRational :: ProblemId -> Rational # | |
Show ProblemId Source # | |
NFData ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Eq ProblemId Source # | |
Ord ProblemId Source # | |
ToJSON ProblemId Source # | |
Monad m => MonadFresh ProblemId (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m ProblemId Source # |