Agda.Syntax.Scope.Monad

The scope checking monad

type ScopeM

Errors

isDatatypeModule

General operations

getCurrentModule

setCurrentModule

withCurrentModule

withCurrentModule'

getNamedScope

getCurrentScope

createModule

modifyScopes

modifyNamedScope

setNamedScope

modifyNamedScopeM

modifyCurrentScope

modifyCurrentScopeM

modifyCurrentNameSpace

setContextPrecedence

getContextPrecedence

withContextPrecedence

getLocalVars

modifyLocalVars

setLocalVars

withLocalVars

Names

freshAbstractName

freshAbstractName_

freshAbstractQName

Resolving names

data ResolvedName

resolveName

resolveName'

resolveModule

getNotation

Binding names

bindVariable

bindName

rebindName

bindModule

bindQModule

Module manipulation operations

stripNoNames

type Out

type WSM

copyScope

applyImportDirectiveM

lookupImportedName

mapImportDir

mapUsing

mapRenaming

openModule_