Agda-2.2.10: A dependently typed functional programming language and proof assistant




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.

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.

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