| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 => Name -> Term -> Type -> 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, Type)
escapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a

Documentation

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

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

add a variable to the context

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

Change the context

underAbstraction :: MonadTCM tcm => Arg Type -> Abs a -> (a -> tcm b) -> tcm b | Source

Go under an abstraction.

underAbstraction_ :: MonadTCM tcm => Abs a -> (a -> tcm b) -> tcm b | Source

Go under an abstract without worrying about the type to add to the context.

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

Add a telescope to the context.

getContext :: MonadTCM tcm => tcm [Arg (Name, Type)] | Source

Get the current context.

getContextArgs :: MonadTCM tcm => tcm Args | Source

Generate [Var n - 1, .., Var 0] for all declarations in the context.

getContextTerms :: MonadTCM tcm => tcm [Term] | Source

getContextTelescope :: MonadTCM tcm => tcm Telescope | Source

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

addCtxs :: MonadTCM tcm => [Name] -> Arg Type -> tcm a -> tcm a | Source

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 => Name -> Term -> Type -> tcm a -> tcm a | Source

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 Type | Source

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

getVarInfo :: MonadTCM tcm => Name -> tcm (Term, 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 a | Source

Produced by Haddock version 2.4.2