Agda.TypeChecking.Monad.Context
- mkContextEntry :: MonadTCM tcm => Arg (Name, Type) -> tcm ContextEntry
- addCtx :: MonadTCM tcm => Name -> Arg Type -> tcm a -> tcm a
- inContext :: MonadTCM tcm => [Arg (Name, Type)] -> tcm a -> tcm a
- underAbstraction :: MonadTCM tcm => Arg Type -> Abs a -> (a -> tcm b) -> tcm b
- underAbstraction_ :: MonadTCM tcm => Abs a -> (a -> tcm b) -> tcm b
- addCtxTel :: MonadTCM tcm => Telescope -> tcm a -> tcm a
- getContext :: MonadTCM tcm => tcm [Arg (Name, Type)]
- getContextArgs :: MonadTCM tcm => tcm Args
- getContextTerms :: MonadTCM tcm => tcm [Term]
- getContextTelescope :: MonadTCM tcm => tcm Telescope
- addCtxs :: MonadTCM tcm => [Name] -> Arg Type -> tcm a -> tcm a
- getContextId :: MonadTCM tcm => tcm [CtxId]
- addLetBinding :: MonadTCM tcm => Relevance -> Name -> Term -> Type -> tcm a -> tcm a
- wakeIrrelevantVars :: MonadTCM tcm => tcm a -> tcm a
- applyRelevanceToContext :: MonadTCM tcm => Relevance -> tcm a -> tcm a
- typeOfBV' :: MonadTCM tcm => Nat -> tcm (Arg Type)
- typeOfBV :: MonadTCM tcm => Nat -> tcm Type
- nameOfBV :: MonadTCM tcm => Nat -> tcm Name
- getVarInfo :: MonadTCM tcm => Name -> tcm (Term, Arg Type)
- escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
Documentation
mkContextEntry :: MonadTCM tcm => Arg (Name, Type) -> tcm ContextEntry
underAbstraction :: MonadTCM tcm => Arg Type -> Abs a -> (a -> tcm b) -> tcm b
Go under an abstraction.
underAbstraction_ :: MonadTCM tcm => Abs a -> (a -> tcm b) -> tcm b
Go under an abstract without worrying about the type to add to the context.
getContext :: MonadTCM tcm => tcm [Arg (Name, Type)]
Get the current context.
getContextArgs :: MonadTCM tcm => tcm Args
Generate [Var n - 1, .., Var 0] for all declarations in the context.
getContextTerms :: MonadTCM tcm => tcm [Term]
getContextTelescope :: MonadTCM tcm => tcm Telescope
addCtxs :: MonadTCM tcm => [Name] -> Arg Type -> tcm a -> tcm a
add a bunch of variables with the same type to the context
getContextId :: MonadTCM tcm => tcm [CtxId]
Check if we are in a compatible context, i.e. an extension of the given context.
addLetBinding :: MonadTCM tcm => Relevance -> Name -> Term -> Type -> tcm a -> tcm a
Add a let bound variable
wakeIrrelevantVars :: MonadTCM tcm => tcm a -> tcm a
Wake up irrelevant variables and make them relevant. For instance, in an irrelevant function argument otherwise irrelevant variables may be used, so they are awoken before type checking the argument.
applyRelevanceToContext :: MonadTCM tcm => Relevance -> tcm a -> tcm a
getVarInfo :: MonadTCM tcm => Name -> tcm (Term, Arg Type)
TODO: move(?)
Get the term corresponding to a named variable. If it is a lambda bound variable the deBruijn index is returned and if it is a let bound variable its definition is returned.
escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a