|
Agda.TypeChecking.Monad.Context |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
|
|
add a variable to the context
|
|
|
Change the context
|
|
|
Go under an abstraction.
|
|
|
Go under an abstract without worrying about the type to add to the context.
|
|
|
Add a telescope to the context.
|
|
|
Get the current context.
|
|
|
Generate [Var n - 1, .., Var 0] for all declarations in the context.
|
|
|
|
|
Get the current context as a Telescope with the specified Hiding.
|
|
|
add a bunch of variables with the same type to the context
|
|
|
Check if we are in a compatible context, i.e. an extension of the given context.
|
|
|
Add a let bound variable
|
|
|
get type of bound variable (i.e. deBruijn index)
|
|
|
|
|
|
|
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.
|
|
|
|
Produced by Haddock version 2.6.0 |