Agda.Syntax.Scope.Base

# Scope representation

data Scope

data NameSpaceId

localNameSpace

nameSpaceAccess

scopeNameSpace

data ScopeInfo

type LocalVars

data NameSpace

type ThingsInScope a

type NamesInScope

type ModulesInScope

data InScopeTag a

class InScope a

inNameSpace

data KindOfName

allKindsOfNames

data AbstractName

data AbstractModule

blockOfLines

# Operations on names

# Operations on name and module maps.

mergeNames

# Operations on name spaces

emptyNameSpace

mapNameSpace

zipNameSpace

mapNameSpaceM

# General operations on scopes

emptyScope

emptyScopeInfo

mapScope

mapScope_

mapScopeM

mapScopeM_

zipScope

zipScope_

filterScope

allNamesInScope

allNamesInScope'

exportedNamesInScope

namesInScope

allThingsInScope

thingsInScope

mergeScope

mergeScopes

# Specific operations on scopes

setScopeAccess

setNameSpace

addNamesToScope

addNameToScope

addModuleToScope

applyImportDirective

renameCanonicalNames

restrictPrivate

removeOnlyQualified

publicModules

everythingInScope

flattenScope

scopeLookup

scopeLookup'

# Inverse look-up

inverseScopeLookup

inverseScopeLookupName

inverseScopeLookupModule