Agda.Syntax.Scope.Monad
type ScopeM
isDatatypeModule
getCurrentModule
setCurrentModule
withCurrentModule
withCurrentModule'
getNamedScope
getCurrentScope
createModule
modifyScopes
modifyNamedScope
setNamedScope
modifyNamedScopeM
modifyCurrentScope
modifyCurrentScopeM
modifyCurrentNameSpace
setContextPrecedence
getContextPrecedence
withContextPrecedence
getLocalVars
modifyLocalVars
setLocalVars
withLocalVars
freshAbstractName
freshAbstractName_
freshAbstractQName
data ResolvedName
resolveName
resolveName'
resolveModule
getNotation
bindVariable
bindName
rebindName
bindModule
bindQModule
stripNoNames
type Out
type WSM
copyScope
applyImportDirectiveM
lookupImportedName
mapImportDir
mapUsing
mapRenaming
openModule_