<!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.Abstract.Name</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-Abstract-Name.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Syntax-Abstract-Name.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.Abstract.Name</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Abstract names should carry unique identifiers and stuff. Not right now though.
</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:Name">Name</a> = <a href="#v:Name">Name</a> {<ul class="subs"><li><a href="#v:nameId">nameId</a> :: <a href="Agda-Syntax-Common.html#t:NameId">NameId</a></li><li><a href="#v:nameConcrete">nameConcrete</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></li><li><a href="#v:nameBindingSite">nameBindingSite</a> :: <a href="Agda-Syntax-Position.html#t:Range">Range</a></li><li><a href="#v:nameFixity">nameFixity</a> :: <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a></li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:QName">QName</a> = <a href="#v:QName">QName</a> {<ul class="subs"><li><a href="#v:qnameModule">qnameModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li><a href="#v:qnameName">qnameName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:QNamed">QNamed</a> a = <a href="#v:QNamed">QNamed</a> {<ul class="subs"><li><a href="#v:qname">qname</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></li><li><a href="#v:qnamed">qnamed</a> :: a</li></ul>}</li><li class="src short"><span class="keyword">newtype</span> <a href="#t:ModuleName">ModuleName</a> = <a href="#v:MName">MName</a> {<ul class="subs"><li><a href="#v:mnameToList">mnameToList</a> :: [<a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>]</li></ul>}</li><li class="src short"><span class="keyword">newtype</span> <a href="#t:AmbiguousQName">AmbiguousQName</a> = <a href="#v:AmbQ">AmbQ</a> {<ul class="subs"><li><a href="#v:unAmbQ">unAmbQ</a> :: [<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>]</li></ul>}</li><li class="src short"><a href="#v:isAnonymousModuleName">isAnonymousModuleName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:withRangesOf">withRangesOf</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> [<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>] -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li class="src short"><a href="#v:withRangesOfQ">withRangesOfQ</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</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 class="src short"><a href="#v:mnameFromList">mnameFromList</a> :: [<a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>] -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li class="src short"><a href="#v:noModuleName">noModuleName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li class="src short"><a href="#v:mkName">mkName</a> :: <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></li><li class="src short"><a href="#v:mkName_">mkName_</a> :: <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></li><li class="src short"><a href="#v:qnameToList">qnameToList</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>]</li><li class="src short"><a href="#v:qnameFromList">qnameFromList</a> :: [<a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>] -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></li><li class="src short"><a href="#v:qnameToMName">qnameToMName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li class="src short"><a href="#v:mnameToQName">mnameToQName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></li><li class="src short"><a href="#v:showQNameId">showQNameId</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</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:qnameToConcrete">qnameToConcrete</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></li><li class="src short"><a href="#v:mnameToConcrete">mnameToConcrete</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></li><li class="src short"><a href="#v:toTopLevelModuleName">toTopLevelModuleName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a></li><li class="src short"><a href="#v:qualifyM">qualifyM</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-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li class="src short"><a href="#v:qualifyQ">qualifyQ</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-Abstract-Name.html#t:QName">QName</a></li><li class="src short"><a href="#v:qualify">qualify</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></li><li class="src short"><a href="#v:isOperator">isOperator</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:isSubModuleOf">isSubModuleOf</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="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:isInModule">isInModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:freshName">freshName</a> :: (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Class.html#t:MonadState">MonadState</a> s m, <a href="Agda-Utils-Fresh.html#t:HasFresh">HasFresh</a> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> s) => <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> m <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></li><li class="src short"><a href="#v:freshName_">freshName_</a> :: (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Class.html#t:MonadState">MonadState</a> s m, <a href="Agda-Utils-Fresh.html#t:HasFresh">HasFresh</a> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> s) => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> m <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></li><li class="src short"><a href="#v:freshNoName">freshNoName</a> :: (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Class.html#t:MonadState">MonadState</a> s m, <a href="Agda-Utils-Fresh.html#t:HasFresh">HasFresh</a> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> s) => <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> m <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></li><li class="src short"><a href="#v:freshNoName_">freshNoName_</a> :: (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Class.html#t:MonadState">MonadState</a> s m, <a href="Agda-Utils-Fresh.html#t:HasFresh">HasFresh</a> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> s) => m <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></li><li class="src short"><a href="#v:nextName">nextName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Name" class="def">Name</a> <a href="src/Agda-Syntax-Abstract-Name.html#Name" class="link">Source</a></p><div class="doc"><p>A name is a unique identifier and a suggestion for a concrete name. The
concrete name contains the source location (if any) of the name. The
source location of the binding site is also recorded.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Name" class="def">Name</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:nameId" class="def">nameId</a> :: <a href="Agda-Syntax-Common.html#t:NameId">NameId</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:nameConcrete" class="def">nameConcrete</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:nameBindingSite" class="def">nameBindingSite</a> :: <a href="Agda-Syntax-Position.html#t:Range">Range</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:nameFixity" class="def">nameFixity</a> :: <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</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:Name" class="caption collapser" onclick="toggleSection('i:Name')">Instances</p><div id="section.i:Name" 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-Abstract-Name.html#t:Name">Name</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-Abstract-Name.html#t:Name">Name</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-Abstract-Name.html#t:Name">Name</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-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/hashable-1.1.2.5/Data-Hashable.html#t:Hashable">Hashable</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</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-Abstract-Name.html#t:Name">Name</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-Abstract-Name.html#t:Name">Name</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-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src">Alpha <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Pretty.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</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-Abstract-Name.html#t:Name">Name</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-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewName">NewName</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>) <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewName">NewName</a> <a href="Agda-Syntax-Concrete.html#t:BoundName">BoundName</a>) <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Free.html#t:Free">Free</a> i, <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> i a) => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> (<a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> i) (<a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>, 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:QName" class="def">QName</a> <a href="src/Agda-Syntax-Abstract-Name.html#QName" class="link">Source</a></p><div class="doc"><p>Qualified names are non-empty lists of names. Equality on qualified names
are just equality on the last name, i.e. the module part is just
for show.
</p><p>The <code><a href="Agda-Syntax-Position.html#t:SetRange">SetRange</a></code> instance for qualified names sets all individual
ranges (including those of the module prefix) to the given one.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:QName" class="def">QName</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:qnameModule" class="def">qnameModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:qnameName" class="def">qnameName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</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:QName" class="caption collapser" onclick="toggleSection('i:QName')">Instances</p><div id="section.i:QName" 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-Abstract-Name.html#t:QName">QName</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-Abstract-Name.html#t:QName">QName</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-Abstract-Name.html#t:QName">QName</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-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/hashable-1.1.2.5/Data-Hashable.html#t:Hashable">Hashable</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Size.html#t:Sized">Sized</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</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-Abstract-Name.html#t:QName">QName</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-Abstract-Name.html#t:QName">QName</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-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Pretty.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</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-Abstract-Name.html#t:QName">QName</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-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Quote.html#t:Unquote">Unquote</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:FromTerm">FromTerm</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:ToTerm">ToTerm</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Primitive.html#t:PrimTerm">PrimTerm</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/geniplate-0.6.0.3/Data-Generics-Geniplate.html#t:UniverseBi">UniverseBi</a> <a href="Agda-Syntax-Abstract.html#t:Declaration">Declaration</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:OldName">OldName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:ShrinkC">ShrinkC</a> <a href="Agda-TypeChecking-Test-Generators.html#t:ConName">ConName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:ShrinkC">ShrinkC</a> <a href="Agda-TypeChecking-Test-Generators.html#t:DefName">DefName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</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-Abstract-Name.html#t:QName">QName</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:Name">Name</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:QNamed" class="def">QNamed</a> a <a href="src/Agda-Syntax-Abstract-Name.html#QNamed" class="link">Source</a></p><div class="doc"><p>Something preceeded by a qualified name.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:QNamed" class="def">QNamed</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:qname" class="def">qname</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:qnamed" class="def">qnamed</a> :: 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:QNamed" class="caption collapser" onclick="toggleSection('i:QNamed')">Instances</p><div id="section.i:QNamed" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Functor">Functor</a> <a href="Agda-Syntax-Abstract-Name.html#t:QNamed">QNamed</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:Typeable1">Typeable1</a> <a href="Agda-Syntax-Abstract-Name.html#t:QNamed">QNamed</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-Foldable.html#t:Foldable">Foldable</a> <a href="Agda-Syntax-Abstract-Name.html#t:QNamed">QNamed</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-Traversable.html#t:Traversable">Traversable</a> <a href="Agda-Syntax-Abstract-Name.html#t:QNamed">QNamed</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Pretty.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:NamedClause">NamedClause</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:NamedClause">NamedClause</a> <a href="Agda-Syntax-Abstract.html#t:Clause">Clause</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 => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> (<a href="Agda-Syntax-Abstract-Name.html#t:QNamed">QNamed</a> a)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">newtype</span> <a name="t:ModuleName" class="def">ModuleName</a> <a href="src/Agda-Syntax-Abstract-Name.html#ModuleName" class="link">Source</a></p><div class="doc"><p>A module name is just a qualified name.
</p><p>The <code><a href="Agda-Syntax-Position.html#t:SetRange">SetRange</a></code> instance for module names sets all individual ranges
to the given one.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:MName" class="def">MName</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:mnameToList" class="def">mnameToList</a> :: [<a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</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:ModuleName" class="caption collapser" onclick="toggleSection('i:ModuleName')">Instances</p><div id="section.i:ModuleName" 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-Abstract-Name.html#t:ModuleName">ModuleName</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-Abstract-Name.html#t:ModuleName">ModuleName</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-Abstract-Name.html#t:ModuleName">ModuleName</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-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Size.html#t:Sized">Sized</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</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-Abstract-Name.html#t:ModuleName">ModuleName</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-Abstract-Name.html#t:ModuleName">ModuleName</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-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Pretty.html#t:PrettyTCM">PrettyTCM</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</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-Abstract-Name.html#t:ModuleName">ModuleName</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-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/geniplate-0.6.0.3/Data-Generics-Geniplate.html#t:UniverseBi">UniverseBi</a> <a href="Agda-Syntax-Abstract.html#t:Declaration">Declaration</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:OldModuleName">OldModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewModuleQName">NewModuleQName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewModuleName">NewModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">newtype</span> <a name="t:AmbiguousQName" class="def">AmbiguousQName</a> <a href="src/Agda-Syntax-Abstract-Name.html#AmbiguousQName" class="link">Source</a></p><div class="doc"><p>Ambiguous qualified names. Used for overloaded constructors.
</p><p>Invariant: All the names in the list must have the same concrete,
unqualified name.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:AmbQ" class="def">AmbQ</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:unAmbQ" class="def">unAmbQ</a> :: [<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</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:AmbiguousQName" class="caption collapser" onclick="toggleSection('i:AmbiguousQName')">Instances</p><div id="section.i:AmbiguousQName" 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-Abstract-Name.html#t:AmbiguousQName">AmbiguousQName</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-Abstract-Name.html#t:AmbiguousQName">AmbiguousQName</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-Abstract-Name.html#t:AmbiguousQName">AmbiguousQName</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-Abstract-Name.html#t:AmbiguousQName">AmbiguousQName</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-Abstract-Name.html#t:AmbiguousQName">AmbiguousQName</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-Abstract-Name.html#t:AmbiguousQName">AmbiguousQName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/geniplate-0.6.0.3/Data-Generics-Geniplate.html#t:UniverseBi">UniverseBi</a> <a href="Agda-Syntax-Abstract.html#t:Declaration">Declaration</a> <a href="Agda-Syntax-Abstract-Name.html#t:AmbiguousQName">AmbiguousQName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:isAnonymousModuleName" class="def">isAnonymousModuleName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Syntax-Abstract-Name.html#isAnonymousModuleName" class="link">Source</a></p><div class="doc"><p>A module is anonymous if the qualification path ends in an underscore.
</p></div></div><div class="top"><p class="src"><a name="v:withRangesOf" class="def">withRangesOf</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> [<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>] -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a><a href="src/Agda-Syntax-Abstract-Name.html#withRangesOf" class="link">Source</a></p><div class="doc"><p>Sets the ranges of the individual names in the module name to
match those of the corresponding concrete names. If the concrete
names are fewer than the number of module name name parts, then the
initial name parts get the range <code><a href="Agda-Syntax-Position.html#v:noRange">noRange</a></code>.
</p><p><code>C.D.E `withRangesOf` [A, B]</code> returns <code>C.D.E</code> but with ranges set
as follows:
</p><ul><li> <code>C</code>: <code><a href="Agda-Syntax-Position.html#v:noRange">noRange</a></code>.
</li><li> <code>D</code>: the range of <code>A</code>.
</li><li> <code>E</code>: the range of <code>B</code>.
</li></ul><p>Precondition: The number of module name name parts has to be at
least as large as the length of the list.
</p></div></div><div class="top"><p class="src"><a name="v:withRangesOfQ" class="def">withRangesOfQ</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a><a href="src/Agda-Syntax-Abstract-Name.html#withRangesOfQ" class="link">Source</a></p><div class="doc"><p>Like <code><a href="Agda-Syntax-Abstract-Name.html#v:withRangesOf">withRangesOf</a></code>, but uses the name parts (qualifier + name)
of the qualified name as the list of concrete names.
</p></div></div><div class="top"><p class="src"><a name="v:mnameFromList" class="def">mnameFromList</a> :: [<a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>] -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a><a href="src/Agda-Syntax-Abstract-Name.html#mnameFromList" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:noModuleName" class="def">noModuleName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a><a href="src/Agda-Syntax-Abstract-Name.html#noModuleName" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mkName" class="def">mkName</a> :: <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a><a href="src/Agda-Syntax-Abstract-Name.html#mkName" class="link">Source</a></p><div class="doc"><p>The <code><a href="Agda-Syntax-Position.html#t:Range">Range</a></code> sets the <em>definition site</em> of the name, not the use
site.
</p></div></div><div class="top"><p class="src"><a name="v:mkName_" class="def">mkName_</a> :: <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a><a href="src/Agda-Syntax-Abstract-Name.html#mkName_" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:qnameToList" class="def">qnameToList</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>]<a href="src/Agda-Syntax-Abstract-Name.html#qnameToList" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:qnameFromList" class="def">qnameFromList</a> :: [<a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a>] -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a><a href="src/Agda-Syntax-Abstract-Name.html#qnameFromList" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:qnameToMName" class="def">qnameToMName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a><a href="src/Agda-Syntax-Abstract-Name.html#qnameToMName" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mnameToQName" class="def">mnameToQName</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="src/Agda-Syntax-Abstract-Name.html#mnameToQName" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:showQNameId" class="def">showQNameId</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</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-Abstract-Name.html#showQNameId" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:qnameToConcrete" class="def">qnameToConcrete</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a><a href="src/Agda-Syntax-Abstract-Name.html#qnameToConcrete" class="link">Source</a></p><div class="doc"><p>Turn a qualified name into a concrete name. This should only be used as a
fallback when looking up the right concrete name in the scope fails.
</p></div></div><div class="top"><p class="src"><a name="v:mnameToConcrete" class="def">mnameToConcrete</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a><a href="src/Agda-Syntax-Abstract-Name.html#mnameToConcrete" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:toTopLevelModuleName" class="def">toTopLevelModuleName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a><a href="src/Agda-Syntax-Abstract-Name.html#toTopLevelModuleName" class="link">Source</a></p><div class="doc"><p>Computes the <code>TopLevelModuleName</code> corresponding to the given
module name, which is assumed to represent a top-level module name.
</p><p>Precondition: The module name must be well-formed.
</p></div></div><div class="top"><p class="src"><a name="v:qualifyM" class="def">qualifyM</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-Abstract-Name.html#t:ModuleName">ModuleName</a><a href="src/Agda-Syntax-Abstract-Name.html#qualifyM" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:qualifyQ" class="def">qualifyQ</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-Abstract-Name.html#t:QName">QName</a><a href="src/Agda-Syntax-Abstract-Name.html#qualifyQ" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:qualify" class="def">qualify</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a><a href="src/Agda-Syntax-Abstract-Name.html#qualify" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isOperator" class="def">isOperator</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Syntax-Abstract-Name.html#isOperator" class="link">Source</a></p><div class="doc"><p>Is the name an operator?
</p></div></div><div class="top"><p class="src"><a name="v:isSubModuleOf" class="def">isSubModuleOf</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="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Syntax-Abstract-Name.html#isSubModuleOf" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isInModule" class="def">isInModule</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Syntax-Abstract-Name.html#isInModule" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:freshName" class="def">freshName</a> :: (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Class.html#t:MonadState">MonadState</a> s m, <a href="Agda-Utils-Fresh.html#t:HasFresh">HasFresh</a> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> s) => <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> m <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a><a href="src/Agda-Syntax-Abstract-Name.html#freshName" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:freshName_" class="def">freshName_</a> :: (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Class.html#t:MonadState">MonadState</a> s m, <a href="Agda-Utils-Fresh.html#t:HasFresh">HasFresh</a> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> s) => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> m <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a><a href="src/Agda-Syntax-Abstract-Name.html#freshName_" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:freshNoName" class="def">freshNoName</a> :: (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Class.html#t:MonadState">MonadState</a> s m, <a href="Agda-Utils-Fresh.html#t:HasFresh">HasFresh</a> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> s) => <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> m <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a><a href="src/Agda-Syntax-Abstract-Name.html#freshNoName" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:freshNoName_" class="def">freshNoName_</a> :: (<a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Class.html#t:MonadState">MonadState</a> s m, <a href="Agda-Utils-Fresh.html#t:HasFresh">HasFresh</a> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> s) => m <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a><a href="src/Agda-Syntax-Abstract-Name.html#freshNoName_" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:nextName" class="def">nextName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a><a href="src/Agda-Syntax-Abstract-Name.html#nextName" class="link">Source</a></p><div class="doc"><p>Get the next version of the concrete name. For instance, <code>nextName <a href="x.html">x</a> = <a href="x₁.html">x₁</a></code>.
The name must not be a <code>NoName</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>
