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




modifyContext :: MonadTCM tcm => (Context -> Context) -> tcm a -> tcm aSource

Modify a Context in a computation.

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

addCtx x arg cont add a variable to the context.

Chooses an unused Name.

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

N-ary variant of addCtx.

addCtxString :: MonadTCM tcm => String -> Arg Type -> tcm a -> tcm aSource

Turns the string into a name and adds it to the context.

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

Change the context

underAbstraction :: (Raise a, MonadTCM tcm) => Arg Type -> Abs a -> (a -> tcm b) -> tcm bSource

Go under an abstraction.

underAbstraction_ :: (Raise a, 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

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