<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda.Syntax.Scope.Base</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Agda-Syntax-Scope-Base.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Syntax-Scope-Base.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr></table><p class="caption">Agda.Syntax.Scope.Base</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">Scope representation
</a></li><li><a href="#g:2">Operations on names
</a></li><li><a href="#g:3">Operations on name and module maps.
</a></li><li><a href="#g:4">Operations on name spaces
</a></li><li><a href="#g:5">General operations on scopes
</a></li><li><a href="#g:6">Specific operations on scopes
</a></li><li><a href="#g:7">Inverse look-up
</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>This module defines the notion of a scope and operations on scopes.
</p></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">data</span> <a href="#t:Scope">Scope</a> = <a href="#v:Scope">Scope</a> {<ul class="subs"><li><a href="#v:scopeName">scopeName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li><a href="#v:scopeParents">scopeParents</a> :: [<a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a>]</li><li><a href="#v:scopeNameSpaces">scopeNameSpaces</a> :: [(<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a>, <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a>)]</li><li><a href="#v:scopeImports">scopeImports</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li><a href="#v:scopeDatatypeModule">scopeDatatypeModule</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:NameSpaceId">NameSpaceId</a> <ul class="subs"><li>= <a href="#v:PrivateNS">PrivateNS</a> </li><li>| <a href="#v:PublicNS">PublicNS</a> </li><li>| <a href="#v:ImportedNS">ImportedNS</a> </li><li>| <a href="#v:OnlyQualifiedNS">OnlyQualifiedNS</a> </li></ul></li><li class="src short"><a href="#v:localNameSpace">localNameSpace</a> :: <a href="Agda-Syntax-Common.html#t:Access">Access</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a></li><li class="src short"><a href="#v:nameSpaceAccess">nameSpaceAccess</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Common.html#t:Access">Access</a></li><li class="src short"><a href="#v:scopeNameSpace">scopeNameSpace</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:ScopeInfo">ScopeInfo</a> = <a href="#v:ScopeInfo">ScopeInfo</a> {<ul class="subs"><li><a href="#v:scopeCurrent">scopeCurrent</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li><a href="#v:scopeModules">scopeModules</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li><a href="#v:scopeLocals">scopeLocals</a> :: <a href="Agda-Syntax-Scope-Base.html#t:LocalVars">LocalVars</a></li><li><a href="#v:scopePrecedence">scopePrecedence</a> :: <a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a></li></ul>}</li><li class="src short"><span class="keyword">type</span> <a href="#t:LocalVars">LocalVars</a> = [(<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>, <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>)]</li><li class="src short"><span class="keyword">data</span> <a href="#t:NameSpace">NameSpace</a> = <a href="#v:NameSpace">NameSpace</a> {<ul class="subs"><li><a href="#v:nsNames">nsNames</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a></li><li><a href="#v:nsModules">nsModules</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a></li></ul>}</li><li class="src short"><span class="keyword">type</span> <a href="#t:ThingsInScope">ThingsInScope</a> a = <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [a]</li><li class="src short"><span class="keyword">type</span> <a href="#t:NamesInScope">NamesInScope</a> = <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:ModulesInScope">ModulesInScope</a> = <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:InScopeTag">InScopeTag</a> a <span class="keyword">where</span><ul class="subs"><li><a href="#v:NameTag">NameTag</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScopeTag">InScopeTag</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a> </li><li><a href="#v:ModuleTag">ModuleTag</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScopeTag">InScopeTag</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a> </li></ul></li><li class="src short"><span class="keyword">class</span> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> a => <a href="#t:InScope">InScope</a> a <span class="keyword">where</span><ul class="subs"><li><a href="#v:inScopeTag">inScopeTag</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScopeTag">InScopeTag</a> a</li></ul></li><li class="src short"><a href="#v:inNameSpace">inNameSpace</a> :: <span class="keyword">forall</span> a. <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a</li><li class="src short"><span class="keyword">data</span> <a href="#t:KindOfName">KindOfName</a> <ul class="subs"><li>= <a href="#v:ConName">ConName</a> </li><li>| <a href="#v:FldName">FldName</a> </li><li>| <a href="#v:DefName">DefName</a> </li><li>| <a href="#v:PatternSynName">PatternSynName</a> </li></ul></li><li class="src short"><a href="#v:allKindsOfNames">allKindsOfNames</a> :: [<a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a>]</li><li class="src short"><span class="keyword">data</span> <a href="#t:AbstractName">AbstractName</a> = <a href="#v:AbsName">AbsName</a> {<ul class="subs"><li><a href="#v:anameName">anameName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></li><li><a href="#v:anameKind">anameKind</a> :: <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a></li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:AbstractModule">AbstractModule</a> = <a href="#v:AbsModule">AbsModule</a> {<ul class="subs"><li><a href="#v:amodName">amodName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li></ul>}</li><li class="src short"><a href="#v:blockOfLines">blockOfLines</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</li><li class="src short"><a href="#v:mergeNames">mergeNames</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> a => <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a</li><li class="src short"><a href="#v:emptyNameSpace">emptyNameSpace</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></li><li class="src short"><a href="#v:mapNameSpace">mapNameSpace</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></li><li class="src short"><a href="#v:zipNameSpace">zipNameSpace</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></li><li class="src short"><a href="#v:mapNameSpaceM">mapNameSpaceM</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> m => (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></li><li class="src short"><a href="#v:emptyScope">emptyScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:emptyScopeInfo">emptyScopeInfo</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a></li><li class="src short"><a href="#v:mapScope">mapScope</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:mapScope_">mapScope_</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:mapScopeM">mapScopeM</a> :: (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Functor">Functor</a> m, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> m) => (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:mapScopeM_">mapScopeM_</a> :: (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Functor">Functor</a> m, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> m) => (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:zipScope">zipScope</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:zipScope_">zipScope_</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:filterScope">filterScope</a> :: (<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>) -> (<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:allNamesInScope">allNamesInScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a</li><li class="src short"><a href="#v:allNamesInScope-39-">allNamesInScope'</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> (a, <a href="Agda-Syntax-Common.html#t:Access">Access</a>)</li><li class="src short"><a href="#v:exportedNamesInScope">exportedNamesInScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a</li><li class="src short"><a href="#v:namesInScope">namesInScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => [<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a>] -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a</li><li class="src short"><a href="#v:allThingsInScope">allThingsInScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></li><li class="src short"><a href="#v:thingsInScope">thingsInScope</a> :: [<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a>] -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></li><li class="src short"><a href="#v:mergeScope">mergeScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:mergeScopes">mergeScopes</a> :: [<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>] -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:setScopeAccess">setScopeAccess</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:setNameSpace">setNameSpace</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:addNamesToScope">addNamesToScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> [<a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a>] -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:addNameToScope">addNameToScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:addModuleToScope">addModuleToScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:applyImportDirective">applyImportDirective</a> :: <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:renameCanonicalNames">renameCanonicalNames</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:restrictPrivate">restrictPrivate</a> :: <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:removeOnlyQualified">removeOnlyQualified</a> :: <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:publicModules">publicModules</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></li><li class="src short"><a href="#v:everythingInScope">everythingInScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></li><li class="src short"><a href="#v:flattenScope">flattenScope</a> :: [[<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>]] -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> [<a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a>]</li><li class="src short"><a href="#v:scopeLookup">scopeLookup</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> [a]</li><li class="src short"><a href="#v:scopeLookup-39-">scopeLookup'</a> :: <span class="keyword">forall</span> a. <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> [(a, <a href="Agda-Syntax-Common.html#t:Access">Access</a>)]</li><li class="src short"><a href="#v:inverseScopeLookup">inverseScopeLookup</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></li><li class="src short"><a href="#v:inverseScopeLookupName">inverseScopeLookupName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></li><li class="src short"><a href="#v:inverseScopeLookupModule">inverseScopeLookupModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></li></ul></div><div id="interface"><h1 id="g:1">Scope representation
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Scope" class="def">Scope</a> <a href="src/Agda-Syntax-Scope-Base.html#Scope" class="link">Source</a></p><div class="doc"><p>A scope is a named collection of names partitioned into public and private
names.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Scope" class="def">Scope</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:scopeName" class="def">scopeName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:scopeParents" class="def">scopeParents</a> :: [<a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a>]</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:scopeNameSpaces" class="def">scopeNameSpaces</a> :: [(<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a>, <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a>)]</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:scopeImports" class="def">scopeImports</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:scopeDatatypeModule" class="def">scopeDatatypeModule</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Scope" class="caption collapser" onclick="toggleSection('i:Scope')">Instances</p><div id="section.i:Scope" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:InstantiateFull">InstantiateFull</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:NameSpaceId" class="def">NameSpaceId</a> <a href="src/Agda-Syntax-Scope-Base.html#NameSpaceId" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:PrivateNS" class="def">PrivateNS</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:PublicNS" class="def">PublicNS</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:ImportedNS" class="def">ImportedNS</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:OnlyQualifiedNS" class="def">OnlyQualifiedNS</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:NameSpaceId" class="caption collapser" onclick="toggleSection('i:NameSpaceId')">Instances</p><div id="section.i:NameSpaceId" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Bounded">Bounded</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Enum">Enum</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:localNameSpace" class="def">localNameSpace</a> :: <a href="Agda-Syntax-Common.html#t:Access">Access</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a><a href="src/Agda-Syntax-Scope-Base.html#localNameSpace" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:nameSpaceAccess" class="def">nameSpaceAccess</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Common.html#t:Access">Access</a><a href="src/Agda-Syntax-Scope-Base.html#nameSpaceAccess" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:scopeNameSpace" class="def">scopeNameSpace</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a><a href="src/Agda-Syntax-Scope-Base.html#scopeNameSpace" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:ScopeInfo" class="def">ScopeInfo</a> <a href="src/Agda-Syntax-Scope-Base.html#ScopeInfo" class="link">Source</a></p><div class="doc"><p>The complete information about the scope at a particular program point
includes the scope stack, the local variables, and the context precedence.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:ScopeInfo" class="def">ScopeInfo</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:scopeCurrent" class="def">scopeCurrent</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:scopeModules" class="def">scopeModules</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:scopeLocals" class="def">scopeLocals</a> :: <a href="Agda-Syntax-Scope-Base.html#t:LocalVars">LocalVars</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:scopePrecedence" class="def">scopePrecedence</a> :: <a href="Agda-Syntax-Fixity.html#t:Precedence">Precedence</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:ScopeInfo" class="caption collapser" onclick="toggleSection('i:ScopeInfo')">Instances</p><div id="section.i:ScopeInfo" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:LocalVars" class="def">LocalVars</a> = [(<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>, <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>)]<a href="src/Agda-Syntax-Scope-Base.html#LocalVars" class="link">Source</a></p><div class="doc"><p>Local variables
</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:NameSpace" class="def">NameSpace</a> <a href="src/Agda-Syntax-Scope-Base.html#NameSpace" class="link">Source</a></p><div class="doc"><p>A <code>NameSpace</code> contains the mappings from concrete names that the user can
write to the abstract fully qualified names that the type checker wants to
read.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NameSpace" class="def">NameSpace</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:nsNames" class="def">nsNames</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:nsModules" class="def">nsModules</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:NameSpace" class="caption collapser" onclick="toggleSection('i:NameSpace')">Instances</p><div id="section.i:NameSpace" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:ThingsInScope" class="def">ThingsInScope</a> a = <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [a]<a href="src/Agda-Syntax-Scope-Base.html#ThingsInScope" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:NamesInScope" class="def">NamesInScope</a> = <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a><a href="src/Agda-Syntax-Scope-Base.html#NamesInScope" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:ModulesInScope" class="def">ModulesInScope</a> = <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a><a href="src/Agda-Syntax-Scope-Base.html#ModulesInScope" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:InScopeTag" class="def">InScopeTag</a> a <span class="keyword">where</span><a href="src/Agda-Syntax-Scope-Base.html#InScopeTag" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NameTag" class="def">NameTag</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScopeTag">InScopeTag</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:ModuleTag" class="def">ModuleTag</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScopeTag">InScopeTag</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">class</span> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> a => <a name="t:InScope" class="def">InScope</a> a <span class="keyword">where</span><a href="src/Agda-Syntax-Scope-Base.html#InScope" class="link">Source</a></p><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:inScopeTag" class="def">inScopeTag</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScopeTag">InScopeTag</a> a<a href="src/Agda-Syntax-Scope-Base.html#inScopeTag" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:InScope" class="caption collapser" onclick="toggleSection('i:InScope')">Instances</p><div id="section.i:InScope" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:inNameSpace" class="def">inNameSpace</a> :: <span class="keyword">forall</span> a. <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a<a href="src/Agda-Syntax-Scope-Base.html#inNameSpace" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:KindOfName" class="def">KindOfName</a> <a href="src/Agda-Syntax-Scope-Base.html#KindOfName" class="link">Source</a></p><div class="doc"><p>We distinguish constructor names from other names.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:ConName" class="def">ConName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:FldName" class="def">FldName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:DefName" class="def">DefName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:PatternSynName" class="def">PatternSynName</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:KindOfName" class="caption collapser" onclick="toggleSection('i:KindOfName')">Instances</p><div id="section.i:KindOfName" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Bounded">Bounded</a> <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Enum">Enum</a> <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:allKindsOfNames" class="def">allKindsOfNames</a> :: [<a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a>]<a href="src/Agda-Syntax-Scope-Base.html#allKindsOfNames" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:AbstractName" class="def">AbstractName</a> <a href="src/Agda-Syntax-Scope-Base.html#AbstractName" class="link">Source</a></p><div class="doc"><p>Apart from the name, we also record whether it's a constructor or not and
what the fixity is.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:AbsName" class="def">AbsName</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:anameName" class="def">anameName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:anameKind" class="def">anameKind</a> :: <a href="Agda-Syntax-Scope-Base.html#t:KindOfName">KindOfName</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:AbstractName" class="caption collapser" onclick="toggleSection('i:AbstractName')">Instances</p><div id="section.i:AbstractName" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:SetRange">SetRange</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:HasRange">HasRange</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:AbstractModule" class="def">AbstractModule</a> <a href="src/Agda-Syntax-Scope-Base.html#AbstractModule" class="link">Source</a></p><div class="doc"><p>For modules we record the arity. I'm not sure that it's every used anywhere.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:AbsModule" class="def">AbsModule</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:amodName" class="def">amodName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:AbstractModule" class="caption collapser" onclick="toggleSection('i:AbstractModule')">Instances</p><div id="section.i:AbstractModule" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable">Typeable</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:blockOfLines" class="def">blockOfLines</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]<a href="src/Agda-Syntax-Scope-Base.html#blockOfLines" class="link">Source</a></p></div><h1 id="g:2">Operations on names
</h1><h1 id="g:3">Operations on name and module maps.
</h1><div class="top"><p class="src"><a name="v:mergeNames" class="def">mergeNames</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> a => <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a<a href="src/Agda-Syntax-Scope-Base.html#mergeNames" class="link">Source</a></p></div><h1 id="g:4">Operations on name spaces
</h1><div class="top"><p class="src"><a name="v:emptyNameSpace" class="def">emptyNameSpace</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a><a href="src/Agda-Syntax-Scope-Base.html#emptyNameSpace" class="link">Source</a></p><div class="doc"><p>The empty name space.
</p></div></div><div class="top"><p class="src"><a name="v:mapNameSpace" class="def">mapNameSpace</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a><a href="src/Agda-Syntax-Scope-Base.html#mapNameSpace" class="link">Source</a></p><div class="doc"><p>Map functions over the names and modules in a name space.
</p></div></div><div class="top"><p class="src"><a name="v:zipNameSpace" class="def">zipNameSpace</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a><a href="src/Agda-Syntax-Scope-Base.html#zipNameSpace" class="link">Source</a></p><div class="doc"><p>Zip together two name spaces.
</p></div></div><div class="top"><p class="src"><a name="v:mapNameSpaceM" class="def">mapNameSpaceM</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> m => (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a><a href="src/Agda-Syntax-Scope-Base.html#mapNameSpaceM" class="link">Source</a></p><div class="doc"><p>Map monadic function over a namespace.
</p></div></div><h1 id="g:5">General operations on scopes
</h1><div class="top"><p class="src"><a name="v:emptyScope" class="def">emptyScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#emptyScope" class="link">Source</a></p><div class="doc"><p>The empty scope.
</p></div></div><div class="top"><p class="src"><a name="v:emptyScopeInfo" class="def">emptyScopeInfo</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a><a href="src/Agda-Syntax-Scope-Base.html#emptyScopeInfo" class="link">Source</a></p><div class="doc"><p>The empty scope info.
</p></div></div><div class="top"><p class="src"><a name="v:mapScope" class="def">mapScope</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#mapScope" class="link">Source</a></p><div class="doc"><p>Map functions over the names and modules in a scope.
</p></div></div><div class="top"><p class="src"><a name="v:mapScope_" class="def">mapScope_</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#mapScope_" class="link">Source</a></p><div class="doc"><p>Same as <code><a href="Agda-Syntax-Scope-Base.html#v:mapScope">mapScope</a></code> but applies the same function to all name spaces.
</p></div></div><div class="top"><p class="src"><a name="v:mapScopeM" class="def">mapScopeM</a> :: (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Functor">Functor</a> m, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> m) => (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#mapScopeM" class="link">Source</a></p><div class="doc"><p>Map monadic functions over the names and modules in a scope.
</p></div></div><div class="top"><p class="src"><a name="v:mapScopeM_" class="def">mapScopeM_</a> :: (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Functor">Functor</a> m, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> m) => (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> m <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#mapScopeM_" class="link">Source</a></p><div class="doc"><p>Same as <code><a href="Agda-Syntax-Scope-Base.html#v:mapScopeM">mapScopeM</a></code> but applies the same function to both the public and
private name spaces.
</p></div></div><div class="top"><p class="src"><a name="v:zipScope" class="def">zipScope</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#zipScope" class="link">Source</a></p><div class="doc"><p>Zip together two scopes. The resulting scope has the same name as the
first scope.
</p></div></div><div class="top"><p class="src"><a name="v:zipScope_" class="def">zipScope_</a> :: (<a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NamesInScope">NamesInScope</a>) -> (<a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ModulesInScope">ModulesInScope</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#zipScope_" class="link">Source</a></p><div class="doc"><p>Same as <code><a href="Agda-Syntax-Scope-Base.html#v:zipScope">zipScope</a></code> but applies the same function to both the public and
private name spaces.
</p></div></div><div class="top"><p class="src"><a name="v:filterScope" class="def">filterScope</a> :: (<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>) -> (<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>) -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#filterScope" class="link">Source</a></p><div class="doc"><p>Filter a scope keeping only concrete names matching the predicates.
The first predicate is applied to the names and the second to the modules.
</p></div></div><div class="top"><p class="src"><a name="v:allNamesInScope" class="def">allNamesInScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a<a href="src/Agda-Syntax-Scope-Base.html#allNamesInScope" class="link">Source</a></p><div class="doc"><p>Return all names in a scope.
</p></div></div><div class="top"><p class="src"><a name="v:allNamesInScope-39-" class="def">allNamesInScope'</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> (a, <a href="Agda-Syntax-Common.html#t:Access">Access</a>)<a href="src/Agda-Syntax-Scope-Base.html#allNamesInScope%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:exportedNamesInScope" class="def">exportedNamesInScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a<a href="src/Agda-Syntax-Scope-Base.html#exportedNamesInScope" class="link">Source</a></p><div class="doc"><p>Returns the scope's non-private names.
</p></div></div><div class="top"><p class="src"><a name="v:namesInScope" class="def">namesInScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => [<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a>] -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ThingsInScope">ThingsInScope</a> a<a href="src/Agda-Syntax-Scope-Base.html#namesInScope" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:allThingsInScope" class="def">allThingsInScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a><a href="src/Agda-Syntax-Scope-Base.html#allThingsInScope" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:thingsInScope" class="def">thingsInScope</a> :: [<a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a>] -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a><a href="src/Agda-Syntax-Scope-Base.html#thingsInScope" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mergeScope" class="def">mergeScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#mergeScope" class="link">Source</a></p><div class="doc"><p>Merge two scopes. The result has the name of the first scope.
</p></div></div><div class="top"><p class="src"><a name="v:mergeScopes" class="def">mergeScopes</a> :: [<a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a>] -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#mergeScopes" class="link">Source</a></p><div class="doc"><p>Merge a non-empty list of scopes. The result has the name of the first
scope in the list.
</p></div></div><h1 id="g:6">Specific operations on scopes
</h1><div class="top"><p class="src"><a name="v:setScopeAccess" class="def">setScopeAccess</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#setScopeAccess" class="link">Source</a></p><div class="doc"><p>Move all names in a scope to the given name space (except never move from
Imported to Public).
</p></div></div><div class="top"><p class="src"><a name="v:setNameSpace" class="def">setNameSpace</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#setNameSpace" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addNamesToScope" class="def">addNamesToScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> [<a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a>] -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#addNamesToScope" class="link">Source</a></p><div class="doc"><p>Add names to a scope.
</p></div></div><div class="top"><p class="src"><a name="v:addNameToScope" class="def">addNameToScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#addNameToScope" class="link">Source</a></p><div class="doc"><p>Add a name to a scope.
</p></div></div><div class="top"><p class="src"><a name="v:addModuleToScope" class="def">addModuleToScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:NameSpaceId">NameSpaceId</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">AbstractModule</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#addModuleToScope" class="link">Source</a></p><div class="doc"><p>Add a module to a scope.
</p></div></div><div class="top"><p class="src"><a name="v:applyImportDirective" class="def">applyImportDirective</a> :: <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#applyImportDirective" class="link">Source</a></p><div class="doc"><p>Apply an <code><a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a></code> to a scope.
</p></div></div><div class="top"><p class="src"><a name="v:renameCanonicalNames" class="def">renameCanonicalNames</a> :: <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#renameCanonicalNames" class="link">Source</a></p><div class="doc"><p>Rename the abstract names in a scope.
</p></div></div><div class="top"><p class="src"><a name="v:restrictPrivate" class="def">restrictPrivate</a> :: <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#restrictPrivate" class="link">Source</a></p><div class="doc"><p>Restrict the private name space of a scope
</p></div></div><div class="top"><p class="src"><a name="v:removeOnlyQualified" class="def">removeOnlyQualified</a> :: <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a> -> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#removeOnlyQualified" class="link">Source</a></p><div class="doc"><p>Remove names that can only be used qualified (when opening a scope)
</p></div></div><div class="top"><p class="src"><a name="v:publicModules" class="def">publicModules</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Scope-Base.html#t:Scope">Scope</a><a href="src/Agda-Syntax-Scope-Base.html#publicModules" class="link">Source</a></p><div class="doc"><p>Get the public parts of the public modules of a scope
</p></div></div><div class="top"><p class="src"><a name="v:everythingInScope" class="def">everythingInScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="Agda-Syntax-Scope-Base.html#t:NameSpace">NameSpace</a><a href="src/Agda-Syntax-Scope-Base.html#everythingInScope" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:flattenScope" class="def">flattenScope</a> :: [[<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>]] -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> [<a href="Agda-Syntax-Scope-Base.html#t:AbstractName">AbstractName</a>]<a href="src/Agda-Syntax-Scope-Base.html#flattenScope" class="link">Source</a></p><div class="doc"><p>Compute a flattened scope. Only include unqualified names or names
qualified by modules in the first argument.
</p></div></div><div class="top"><p class="src"><a name="v:scopeLookup" class="def">scopeLookup</a> :: <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> [a]<a href="src/Agda-Syntax-Scope-Base.html#scopeLookup" class="link">Source</a></p><div class="doc"><p>Look up a name in the scope
</p></div></div><div class="top"><p class="src"><a name="v:scopeLookup-39-" class="def">scopeLookup'</a> :: <span class="keyword">forall</span> a. <a href="Agda-Syntax-Scope-Base.html#t:InScope">InScope</a> a => <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> [(a, <a href="Agda-Syntax-Common.html#t:Access">Access</a>)]<a href="src/Agda-Syntax-Scope-Base.html#scopeLookup%27" class="link">Source</a></p></div><h1 id="g:7">Inverse look-up
</h1><div class="top"><p class="src"><a name="v:inverseScopeLookup" class="def">inverseScopeLookup</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a><a href="src/Agda-Syntax-Scope-Base.html#inverseScopeLookup" class="link">Source</a></p><div class="doc"><p>Find the shortest concrete name that maps (uniquely) to a given abstract
name.
</p></div></div><div class="top"><p class="src"><a name="v:inverseScopeLookupName" class="def">inverseScopeLookupName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a><a href="src/Agda-Syntax-Scope-Base.html#inverseScopeLookupName" class="link">Source</a></p><div class="doc"><p>Takes the first component of <code><a href="Agda-Syntax-Scope-Base.html#v:inverseScopeLookup">inverseScopeLookup</a></code>.
</p></div></div><div class="top"><p class="src"><a name="v:inverseScopeLookupModule" class="def">inverseScopeLookupModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a><a href="src/Agda-Syntax-Scope-Base.html#inverseScopeLookupModule" class="link">Source</a></p><div class="doc"><p>Takes the second component of <code><a href="Agda-Syntax-Scope-Base.html#v:inverseScopeLookup">inverseScopeLookup</a></code>.
</p></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
