Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Monad.Context
Synopsis
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 ContextEntrySource
addCtx :: MonadTCM tcm => Name -> Arg Type -> tcm a -> tcm aSource
add a variable to the context
inContext :: MonadTCM tcm => [Arg (Name, Type)] -> tcm a -> tcm aSource
Change the context
underAbstraction :: MonadTCM tcm => Arg Type -> Abs a -> (a -> tcm b) -> tcm bSource
Go under an abstraction.
underAbstraction_ :: MonadTCM tcm => Abs a -> (a -> tcm b) -> tcm bSource
Go under an abstract without worrying about the type to add to the context.
addCtxTel :: MonadTCM tcm => Telescope -> tcm a -> tcm aSource
Add a telescope to the context.
getContext :: MonadTCM tcm => tcm [Arg (Name, Type)]Source
Get the current context.
getContextArgs :: MonadTCM tcm => tcm ArgsSource
Generate [Var n - 1, .., Var 0] for all declarations in the context.
getContextTerms :: MonadTCM tcm => tcm [Term]Source
getContextTelescope :: MonadTCM tcm => tcm TelescopeSource
Get the current context as a Telescope with the specified Hiding.
addCtxs :: MonadTCM tcm => [Name] -> Arg Type -> tcm a -> tcm aSource
add a bunch of variables with the same type to the context
getContextId :: MonadTCM tcm => tcm [CtxId]Source
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 aSource
Add a let bound variable
wakeIrrelevantVars :: MonadTCM tcm => tcm a -> tcm aSource
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 aSource
typeOfBV' :: MonadTCM tcm => Nat -> tcm (Arg Type)Source
get type of bound variable (i.e. deBruijn index)
typeOfBV :: MonadTCM tcm => Nat -> tcm TypeSource
nameOfBV :: MonadTCM tcm => Nat -> tcm NameSource
getVarInfo :: MonadTCM tcm => Name -> tcm (Term, Arg Type)Source

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 aSource
Produced by Haddock version 2.6.1