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

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

scopeLookup

scopeLookup'

Inverse look-up

inverseScopeLookup

inverseScopeLookupName

inverseScopeLookupModule