Agda.TypeChecking.Monad.Context

Documentation

mkContextEntry :: MonadTCM tcm => Arg (Name, Type) -> tcm ContextEntry

addCtx :: MonadTCM tcm => Name -> Arg Type -> tcm a -> tcm a

add a variable to the context

inContext :: MonadTCM tcm => [Arg (Name, Type)] -> tcm a -> tcm a

Change the context

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.

addCtxTel :: MonadTCM tcm => Telescope -> tcm a -> tcm a

Add a telescope 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

Get the current context as a Telescope with the specified Hiding.

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

typeOfBV' :: MonadTCM tcm => Nat -> tcm (Arg Type)

get type of bound variable (i.e. deBruijn index)

typeOfBV :: MonadTCM tcm => Nat -> tcm Type

nameOfBV :: MonadTCM tcm => Nat -> tcm Name

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