Agda.TypeChecking.Monad.Context

Modifying the context

modifyContextEntry

modifyContextEntries

modifyContext

mkContextEntry

inContext

inTopContext

escapeContext

Adding to the context

addCtx

class AddContext b

addCtxs

addCtxString

addCtxString_

addCtxStrings_

dummyDom

underAbstraction

underAbstraction_

addCtxTel

addLetBinding

Querying the context

getContext

getContextSize

getContextArgs

getContextTerms

getContextTelescope

getContextId

getContextNames

lookupBV

typeOfBV'

typeOfBV

nameOfBV

getVarInfo