Agda.Syntax.Scope.Monad

# The scope checking monad

type ScopeM

# Errors

notInScope

isDatatypeModule

# General operations

getCurrentModule

setCurrentModule

withCurrentModule

withCurrentModule'

getNamedScope

getCurrentScope

createModule

modifyScopeInfo

modifyScopes

modifyNamedScope

modifyCurrentScope

modifyNamedScopeM

modifyCurrentScopeM

modifyCurrentNameSpace

setContextPrecedence

getContextPrecedence

withContextPrecedence

getLocalVars

setLocalVars

withLocalVars

# Names

freshAbstractName

freshAbstractName_

freshAbstractQName

# Resolving names

data ResolvedName

resolveName

resolveModule

getFixity

# Binding names

bindVariable

bindName

bindModule

bindQModule

# Module manipulation operations

stripNoNames

type Ren a

type Out

type WSM

copyScope

applyImportDirectiveM

openModule_