<!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.Common</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-Common.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Syntax-Common.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.Common</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">Relevance
</a></li><li><a href="#g:2">Function type domain
</a></li><li><a href="#g:3">Argument decoration
</a></li><li><a href="#g:4">Named arguments
</a></li><li><a href="#g:5">Infixity, access, abstract, etc.
</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Some common syntactic entities are defined in this module.
</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:Delayed">Delayed</a> <ul class="subs"><li>= <a href="#v:Delayed">Delayed</a> </li><li>| <a href="#v:NotDelayed">NotDelayed</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:Induction">Induction</a> <ul class="subs"><li>= <a href="#v:Inductive">Inductive</a> </li><li>| <a href="#v:CoInductive">CoInductive</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:Hiding">Hiding</a> <ul class="subs"><li>= <a href="#v:Hidden">Hidden</a> </li><li>| <a href="#v:Instance">Instance</a> </li><li>| <a href="#v:NotHidden">NotHidden</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:Relevance">Relevance</a> <ul class="subs"><li>= <a href="#v:Relevant">Relevant</a> </li><li>| <a href="#v:NonStrict">NonStrict</a> </li><li>| <a href="#v:Irrelevant">Irrelevant</a> </li><li>| <a href="#v:Forced">Forced</a> </li><li>| <a href="#v:UnusedArg">UnusedArg</a> </li></ul></li><li class="src short"><a href="#v:moreRelevant">moreRelevant</a> :: <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> -> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</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"><span class="keyword">data</span> <a href="#t:Dom">Dom</a> e = <a href="#v:Dom">Dom</a> {<ul class="subs"><li><a href="#v:domHiding">domHiding</a> :: <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a></li><li><a href="#v:domRelevance">domRelevance</a> :: <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a></li><li><a href="#v:unDom">unDom</a> :: e</li></ul>}</li><li class="src short"><a href="#v:argFromDom">argFromDom</a> :: <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a</li><li class="src short"><a href="#v:domFromArg">domFromArg</a> :: <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a</li><li class="src short"><a href="#v:mapDomHiding">mapDomHiding</a> :: (<a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> -> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a>) -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a</li><li class="src short"><a href="#v:mapDomRelevance">mapDomRelevance</a> :: (<a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> -> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a>) -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a</li><li class="src short"><span class="keyword">data</span> <a href="#t:Arg">Arg</a> e = <a href="#v:Arg">Arg</a> {<ul class="subs"><li><a href="#v:argHiding">argHiding</a> :: <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a></li><li><a href="#v:argRelevance">argRelevance</a> :: <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a></li><li><a href="#v:unArg">unArg</a> :: e</li></ul>}</li><li class="src short"><a href="#v:mapArgHiding">mapArgHiding</a> :: (<a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> -> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a>) -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a</li><li class="src short"><a href="#v:mapArgRelevance">mapArgRelevance</a> :: (<a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> -> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a>) -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a</li><li class="src short"><a href="#v:makeInstance">makeInstance</a> :: <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a</li><li class="src short"><a href="#v:hide">hide</a> :: <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a</li><li class="src short"><a href="#v:defaultArg">defaultArg</a> :: a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a</li><li class="src short"><a href="#v:isHiddenArg">isHiddenArg</a> :: <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> 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:withArgsFrom">withArgsFrom</a> :: [a] -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> b] -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a]</li><li class="src short"><span class="keyword">data</span> <a href="#t:Named">Named</a> name a = <a href="#v:Named">Named</a> {<ul class="subs"><li><a href="#v:nameOf">nameOf</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> name</li><li><a href="#v:namedThing">namedThing</a> :: a</li></ul>}</li><li class="src short"><a href="#v:unnamed">unnamed</a> :: a -> <a href="Agda-Syntax-Common.html#t:Named">Named</a> name a</li><li class="src short"><a href="#v:named">named</a> :: name -> a -> <a href="Agda-Syntax-Common.html#t:Named">Named</a> name a</li><li class="src short"><span class="keyword">type</span> <a href="#t:NamedArg">NamedArg</a> a = <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> a)</li><li class="src short"><a href="#v:namedArg">namedArg</a> :: <a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> a -> a</li><li class="src short"><a href="#v:defaultNamedArg">defaultNamedArg</a> :: a -> <a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> a</li><li class="src short"><a href="#v:updateNamedArg">updateNamedArg</a> :: (a -> b) -> <a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> a -> <a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> b</li><li class="src short"><span class="keyword">data</span> <a href="#t:IsInfix">IsInfix</a> <ul class="subs"><li>= <a href="#v:InfixDef">InfixDef</a> </li><li>| <a href="#v:PrefixDef">PrefixDef</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:Access">Access</a> <ul class="subs"><li>= <a href="#v:PrivateAccess">PrivateAccess</a> </li><li>| <a href="#v:PublicAccess">PublicAccess</a> </li><li>| <a href="#v:OnlyQualified">OnlyQualified</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:IsAbstract">IsAbstract</a> <ul class="subs"><li>= <a href="#v:AbstractDef">AbstractDef</a> </li><li>| <a href="#v:ConcreteDef">ConcreteDef</a> </li></ul></li><li class="src short"><span class="keyword">type</span> <a href="#t:Nat">Nat</a> = <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:Arity">Arity</a> = <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:NameId">NameId</a> = <a href="#v:NameId">NameId</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></li><li class="src short"><span class="keyword">newtype</span> <a href="#t:Constr">Constr</a> a = <a href="#v:Constr">Constr</a> a</li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Delayed" class="def">Delayed</a> <a href="src/Agda-Syntax-Common.html#Delayed" class="link">Source</a></p><div class="doc"><p>Used to specify whether something should be delayed.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Delayed" class="def">Delayed</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:NotDelayed" class="def">NotDelayed</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Delayed" class="caption collapser" onclick="toggleSection('i:Delayed')">Instances</p><div id="section.i:Delayed" 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-Common.html#t:Delayed">Delayed</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-Common.html#t:Delayed">Delayed</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-Common.html#t:Delayed">Delayed</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-Common.html#t:Delayed">Delayed</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-Common.html#t:Delayed">Delayed</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-Common.html#t:Delayed">Delayed</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:Induction" class="def">Induction</a> <a href="src/Agda-Syntax-Common.html#Induction" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Inductive" class="def">Inductive</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CoInductive" class="def">CoInductive</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Induction" class="caption collapser" onclick="toggleSection('i:Induction')">Instances</p><div id="section.i:Induction" 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-Common.html#t:Induction">Induction</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-Common.html#t:Induction">Induction</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-Common.html#t:Induction">Induction</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-Common.html#t:Induction">Induction</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/QuickCheck-2.5.1.1/Test-QuickCheck-Arbitrary.html#t:Arbitrary">Arbitrary</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/QuickCheck-2.5.1.1/Test-QuickCheck-Arbitrary.html#t:CoArbitrary">CoArbitrary</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</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-Common.html#t:Induction">Induction</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-Common.html#t:Induction">Induction</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-Common.html#t:Induction">Induction</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:Hiding" class="def">Hiding</a> <a href="src/Agda-Syntax-Common.html#Hiding" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Hidden" class="def">Hidden</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Instance" class="def">Instance</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:NotHidden" class="def">NotHidden</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Hiding" class="caption collapser" onclick="toggleSection('i:Hiding')">Instances</p><div id="section.i:Hiding" 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-Common.html#t:Hiding">Hiding</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-Common.html#t:Hiding">Hiding</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-Common.html#t:Hiding">Hiding</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-Common.html#t:Hiding">Hiding</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-Common.html#t:Hiding">Hiding</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-Common.html#t:Hiding">Hiding</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-Common.html#t:Hiding">Hiding</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:GenC">GenC</a> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</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-Syntax-Common.html#t:Hiding">Hiding</a> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a></td><td class="doc empty"> </td></tr></table></div></div></div><h1 id="g:1">Relevance
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Relevance" class="def">Relevance</a> <a href="src/Agda-Syntax-Common.html#Relevance" class="link">Source</a></p><div class="doc"><p>A function argument can be relevant or irrelevant.
See <code><a href="Agda-TypeChecking.html#t:Irrelevance">Irrelevance</a></code>.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Relevant" class="def">Relevant</a></td><td class="doc"><p>The argument is (possibly) relevant at compile-time.
</p></td></tr><tr><td class="src"><a name="v:NonStrict" class="def">NonStrict</a></td><td class="doc"><p>The argument may never flow into evaluation position.
Therefore, it is irrelevant at run-time.
It is treated relevantly during equality checking.
</p></td></tr><tr><td class="src"><a name="v:Irrelevant" class="def">Irrelevant</a></td><td class="doc"><p>The argument is irrelevant at compile- and runtime.
</p></td></tr><tr><td class="src"><a name="v:Forced" class="def">Forced</a></td><td class="doc"><p>The argument can be skipped during equality checking
because its value is already determined by the type.
</p></td></tr><tr><td class="src"><a name="v:UnusedArg" class="def">UnusedArg</a></td><td class="doc"><p>The polarity checker has determined that this argument
is unused in the definition. It can be skipped during
equality checking but should be mined for solutions
of meta-variables with relevance <code><a href="Agda-Syntax-Common.html#v:UnusedArg">UnusedArg</a></code>
</p></td></tr></table></div><div class="subs instances"><p id="control.i:Relevance" class="caption collapser" onclick="toggleSection('i:Relevance')">Instances</p><div id="section.i:Relevance" 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-Common.html#t:Relevance">Relevance</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-Common.html#t:Relevance">Relevance</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-Common.html#t:Relevance">Relevance</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-Common.html#t:Relevance">Relevance</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-Common.html#t:Relevance">Relevance</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-Common.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/QuickCheck-2.5.1.1/Test-QuickCheck-Arbitrary.html#t:Arbitrary">Arbitrary</a> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</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-Common.html#t:Relevance">Relevance</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-Common.html#t:Relevance">Relevance</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-Common.html#t:Relevance">Relevance</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-Common.html#t:Relevance">Relevance</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:moreRelevant" class="def">moreRelevant</a> :: <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> -> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</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-Common.html#moreRelevant" class="link">Source</a></p><div class="doc"><p>Information ordering.
<code>Relevant `moreRelevant`
UnusedArg `moreRelevant`
Forced `moreRelevant`
NonStrict `moreRelevant`
Irrelevant</code>
</p></div></div><h1 id="g:2">Function type domain
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Dom" class="def">Dom</a> e <a href="src/Agda-Syntax-Common.html#Dom" class="link">Source</a></p><div class="doc"><p>Similar to <code><a href="Agda-Syntax-Common.html#t:Arg">Arg</a></code>, but we need to distinguish
an irrelevance annotation in a function domain
(the domain itself is not irrelevant!)
from an irrelevant argument.
</p><p><code>Dom</code> is used in <code>Pi</code> of internal syntax, in <code>Context</code> and <code>Telescope</code>.
<code><a href="Agda-Syntax-Common.html#t:Arg">Arg</a></code> is used for actual arguments (<code>Var</code>, <code>Con</code>, <code>Def</code> etc.)
and in <code>Abstract</code> syntax and other situations.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Dom" class="def">Dom</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:domHiding" class="def">domHiding</a> :: <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:domRelevance" class="def">domRelevance</a> :: <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:unDom" class="def">unDom</a> :: e</dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Dom" class="caption collapser" onclick="toggleSection('i:Dom')">Instances</p><div id="section.i:Dom" 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-Common.html#t:Dom">Dom</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-Common.html#t:Dom">Dom</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-Common.html#t:Dom">Dom</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-Common.html#t:Dom">Dom</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Abstract</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</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-Internal.html#t:Telescope">Telescope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-DropArgs.html#t:DropArgs">DropArgs</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a></td><td class="doc"><p>NOTE: This creates telescopes with unbound de Bruijn indices.
</p></td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:Reduce">Reduce</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:Instantiate">Instantiate</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</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-Internal.html#t:Telescope">Telescope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:KillVar">KillVar</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:GenC">GenC</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</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-Internal.html#t:Telescope">Telescope</a> <a href="Agda-Syntax-Abstract.html#t:Telescope">Telescope</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-Syntax-Internal.html#t:Telescope">Telescope</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</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> e => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> e)</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> e => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> e)</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-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Size.html#t:Sized">Sized</a> a => <a href="Agda-Utils-Size.html#t:Sized">Sized</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> a => <a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:HasRange">HasRange</a> a => <a href="Agda-Syntax-Position.html#t:HasRange">HasRange</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Internal-Generic.html#t:TermLike">TermLike</a> a => <a href="Agda-Syntax-Internal-Generic.html#t:TermLike">TermLike</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Abstract.html#t:AbstractTerm">AbstractTerm</a> a => <a href="Agda-TypeChecking-Abstract.html#t:AbstractTerm">AbstractTerm</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> a e, <a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> e c, <a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> c) => <a href="Agda-TypeChecking-Pretty.html#t:PrettyTCM">PrettyTCM</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:InstantiateFull">InstantiateFull</a> t => <a href="Agda-TypeChecking-Reduce.html#t:InstantiateFull">InstantiateFull</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:Normalise">Normalise</a> t => <a href="Agda-TypeChecking-Reduce.html#t:Normalise">Normalise</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:Reduce">Reduce</a> t => <a href="Agda-TypeChecking-Reduce.html#t:Reduce">Reduce</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:Instantiate">Instantiate</a> t => <a href="Agda-TypeChecking-Reduce.html#t:Instantiate">Instantiate</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Mention.html#t:MentionsMeta">MentionsMeta</a> t => <a href="Agda-TypeChecking-MetaVars-Mention.html#t:MentionsMeta">MentionsMeta</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> a => <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Positivity.html#t:ComputeOccurrences">ComputeOccurrences</a> a => <a href="Agda-TypeChecking-Positivity.html#t:ComputeOccurrences">ComputeOccurrences</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Polarity.html#t:HasPolarity">HasPolarity</a> a => <a href="Agda-TypeChecking-Polarity.html#t:HasPolarity">HasPolarity</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:KillVar">KillVar</a> a => <a href="Agda-TypeChecking-Test-Generators.html#t:KillVar">KillVar</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:GenC">GenC</a> a => <a href="Agda-TypeChecking-Test-Generators.html#t:GenC">GenC</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><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-Common.html#t:Dom">Dom</a> i) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> a b => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a) (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> b)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:ShrinkC">ShrinkC</a> a b => <a href="Agda-TypeChecking-Test-Generators.html#t:ShrinkC">ShrinkC</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a) (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> b)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:argFromDom" class="def">argFromDom</a> :: <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a<a href="src/Agda-Syntax-Common.html#argFromDom" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:domFromArg" class="def">domFromArg</a> :: <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a<a href="src/Agda-Syntax-Common.html#domFromArg" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mapDomHiding" class="def">mapDomHiding</a> :: (<a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> -> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a>) -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a<a href="src/Agda-Syntax-Common.html#mapDomHiding" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mapDomRelevance" class="def">mapDomRelevance</a> :: (<a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> -> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a>) -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a -> <a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a<a href="src/Agda-Syntax-Common.html#mapDomRelevance" class="link">Source</a></p></div><h1 id="g:3">Argument decoration
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Arg" class="def">Arg</a> e <a href="src/Agda-Syntax-Common.html#Arg" class="link">Source</a></p><div class="doc"><p>A function argument can be hidden and/or irrelevant.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Arg" class="def">Arg</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:argHiding" class="def">argHiding</a> :: <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:argRelevance" class="def">argRelevance</a> :: <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:unArg" class="def">unArg</a> :: e</dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Arg" class="caption collapser" onclick="toggleSection('i:Arg')">Instances</p><div id="section.i:Arg" 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-Common.html#t:Arg">Arg</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-Common.html#t:Arg">Arg</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-Common.html#t:Arg">Arg</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-Common.html#t:Arg">Arg</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-Internal.html#t:Args">Args</a> <a href="Agda-Syntax-Internal.html#t:Pattern">Pattern</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-Internal.html#t:Args">Args</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</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 => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> 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> e => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> e)</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-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Size.html#t:Sized">Sized</a> a => <a href="Agda-Utils-Size.html#t:Sized">Sized</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> e => <a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> e)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> a => <a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:HasRange">HasRange</a> a => <a href="Agda-Syntax-Position.html#t:HasRange">HasRange</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Internal-Generic.html#t:TermLike">TermLike</a> a => <a href="Agda-Syntax-Internal-Generic.html#t:TermLike">TermLike</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> a => <a href="Agda-TypeChecking-Substitute.html#t:Subst">Subst</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Abstract.html#t:AbstractTerm">AbstractTerm</a> a => <a href="Agda-TypeChecking-Abstract.html#t:AbstractTerm">AbstractTerm</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">Alpha a => Alpha (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">Rename a => Rename (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> a e, <a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> e c, <a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> c) => <a href="Agda-TypeChecking-Pretty.html#t:PrettyTCM">PrettyTCM</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:InstantiateFull">InstantiateFull</a> t => <a href="Agda-TypeChecking-Reduce.html#t:InstantiateFull">InstantiateFull</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:Normalise">Normalise</a> t => <a href="Agda-TypeChecking-Reduce.html#t:Normalise">Normalise</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:Reduce">Reduce</a> t => <a href="Agda-TypeChecking-Reduce.html#t:Reduce">Reduce</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Reduce.html#t:Instantiate">Instantiate</a> t => <a href="Agda-TypeChecking-Reduce.html#t:Instantiate">Instantiate</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-DisplayForm.html#t:Match">Match</a> a => <a href="Agda-TypeChecking-DisplayForm.html#t:Match">Match</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">DotVars a => DotVars (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Mention.html#t:MentionsMeta">MentionsMeta</a> t => <a href="Agda-TypeChecking-MetaVars-Mention.html#t:MentionsMeta">MentionsMeta</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> a => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> a => <a href="Agda-TypeChecking-MetaVars-Occurs.html#t:Occurs">Occurs</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Positivity.html#t:ComputeOccurrences">ComputeOccurrences</a> a => <a href="Agda-TypeChecking-Positivity.html#t:ComputeOccurrences">ComputeOccurrences</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Polarity.html#t:HasPolarity">HasPolarity</a> a => <a href="Agda-TypeChecking-Polarity.html#t:HasPolarity">HasPolarity</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Quote.html#t:Unquote">Unquote</a> a => <a href="Agda-TypeChecking-Quote.html#t:Unquote">Unquote</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">StripAllProjections a => StripAllProjections (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:KillVar">KillVar</a> a => <a href="Agda-TypeChecking-Test-Generators.html#t:KillVar">KillVar</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:GenC">GenC</a> a => <a href="Agda-TypeChecking-Test-Generators.html#t:GenC">GenC</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> a => <a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> a c => <a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> c)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> c) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> i a => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> i) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc"><p>Skip reification of implicit and irrelevant args if option is off.
</p></td></tr><tr><td class="src"><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-Common.html#t:Dom">Dom</a> i) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> i a => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> i) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> a b => <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH">SubstHH</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> b)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Test-Generators.html#t:ShrinkC">ShrinkC</a> a b => <a href="Agda-TypeChecking-Test-Generators.html#t:ShrinkC">ShrinkC</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> b)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:mapArgHiding" class="def">mapArgHiding</a> :: (<a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> -> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a>) -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a<a href="src/Agda-Syntax-Common.html#mapArgHiding" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mapArgRelevance" class="def">mapArgRelevance</a> :: (<a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> -> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a>) -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a<a href="src/Agda-Syntax-Common.html#mapArgRelevance" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:makeInstance" class="def">makeInstance</a> :: <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a<a href="src/Agda-Syntax-Common.html#makeInstance" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hide" class="def">hide</a> :: <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a<a href="src/Agda-Syntax-Common.html#hide" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:defaultArg" class="def">defaultArg</a> :: a -> <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a<a href="src/Agda-Syntax-Common.html#defaultArg" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isHiddenArg" class="def">isHiddenArg</a> :: <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> 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-Common.html#isHiddenArg" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:withArgsFrom" class="def">withArgsFrom</a> :: [a] -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> b] -> [<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a]<a href="src/Agda-Syntax-Common.html#withArgsFrom" class="link">Source</a></p><div class="doc"><p><code>xs `withArgsFrom` args</code> translates <code>xs</code> into a list of <code><a href="Agda-Syntax-Common.html#t:Arg">Arg</a></code>s,
using the elements in <code>args</code> to fill in the non-<code><a href="Agda-Syntax-Common.html#v:unArg">unArg</a></code> fields.
</p><p>Precondition: The two lists should have equal length.
</p></div></div><h1 id="g:4">Named arguments
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Named" class="def">Named</a> name a <a href="src/Agda-Syntax-Common.html#Named" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Named" class="def">Named</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:nameOf" class="def">nameOf</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> name</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:namedThing" class="def">namedThing</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:Named" class="caption collapser" onclick="toggleSection('i:Named')">Instances</p><div id="section.i:Named" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Typeable-Internal.html#t:Typeable2">Typeable2</a> <a href="Agda-Syntax-Common.html#t:Named">Named</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/Control-Monad.html#t:Functor">Functor</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> name)</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-Common.html#t:Named">Named</a> name)</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-Common.html#t:Named">Named</a> name)</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> name, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> a) => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> 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> name, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> a) => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Ord.html#t:Ord">Ord</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> 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 => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Size.html#t:Sized">Sized</a> a => <a href="Agda-Utils-Size.html#t:Sized">Sized</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> name a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> e => <a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> e)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> a => <a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> name a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:HasRange">HasRange</a> a => <a href="Agda-Syntax-Position.html#t:HasRange">HasRange</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> 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-Eq.html#t:Eq">Eq</a> n, Alpha a) => Alpha (<a href="Agda-Syntax-Common.html#t:Named">Named</a> n a)</td><td class="doc empty"> </td></tr><tr><td class="src">Rename a => Rename (<a href="Agda-Syntax-Common.html#t:Named">Named</a> n a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-Syntax-Translation-InternalToAbstract.html#t:Reify">Reify</a> a e, <a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> e c, <a href="Agda-Utils-Pretty.html#t:Pretty">Pretty</a> c) => <a href="Agda-TypeChecking-Pretty.html#t:PrettyTCM">PrettyTCM</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">DotVars a => DotVars (<a href="Agda-Syntax-Common.html#t:Named">Named</a> s a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> s, <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> t) => <a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">EmbPrj</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> s t)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> a => <a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> 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 c => <a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> name a) (<a href="Agda-Syntax-Common.html#t:Named">Named</a> name c)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> name c) (<a href="Agda-Syntax-Common.html#t:Named">Named</a> name a)</td><td class="doc empty"> </td></tr><tr><td class="src"><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-Common.html#t:Named">Named</a> n i) (<a href="Agda-Syntax-Common.html#t:Named">Named</a> n a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> i a => <a href="Agda-Syntax-Translation-InternalToAbstract.html#t:ReifyWhen">ReifyWhen</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> n i) (<a href="Agda-Syntax-Common.html#t:Named">Named</a> n a)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:unnamed" class="def">unnamed</a> :: a -> <a href="Agda-Syntax-Common.html#t:Named">Named</a> name a<a href="src/Agda-Syntax-Common.html#unnamed" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:named" class="def">named</a> :: name -> a -> <a href="Agda-Syntax-Common.html#t:Named">Named</a> name a<a href="src/Agda-Syntax-Common.html#named" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:NamedArg" class="def">NamedArg</a> a = <a href="Agda-Syntax-Common.html#t:Arg">Arg</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> a)<a href="src/Agda-Syntax-Common.html#NamedArg" class="link">Source</a></p><div class="doc"><p>Only <code><a href="Agda-Syntax-Common.html#v:Hidden">Hidden</a></code> arguments can have names.
</p></div></div><div class="top"><p class="src"><a name="v:namedArg" class="def">namedArg</a> :: <a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> a -> a<a href="src/Agda-Syntax-Common.html#namedArg" class="link">Source</a></p><div class="doc"><p>Get the content of a <code><a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a></code>.
</p></div></div><div class="top"><p class="src"><a name="v:defaultNamedArg" class="def">defaultNamedArg</a> :: a -> <a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> a<a href="src/Agda-Syntax-Common.html#defaultNamedArg" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:updateNamedArg" class="def">updateNamedArg</a> :: (a -> b) -> <a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> a -> <a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> b<a href="src/Agda-Syntax-Common.html#updateNamedArg" class="link">Source</a></p><div class="doc"><p>The functor instance for <code><a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a></code> would be ambiguous,
so we give it another name here.
</p></div></div><h1 id="g:5">Infixity, access, abstract, etc.
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:IsInfix" class="def">IsInfix</a> <a href="src/Agda-Syntax-Common.html#IsInfix" class="link">Source</a></p><div class="doc"><p>Functions can be defined in both infix and prefix style. See
<code><a href="Agda-Syntax-Concrete.html#t:LHS">LHS</a></code>.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:InfixDef" class="def">InfixDef</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:PrefixDef" class="def">PrefixDef</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:IsInfix" class="caption collapser" onclick="toggleSection('i:IsInfix')">Instances</p><div id="section.i:IsInfix" 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-Common.html#t:IsInfix">IsInfix</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-Common.html#t:IsInfix">IsInfix</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-Common.html#t:IsInfix">IsInfix</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-Common.html#t:IsInfix">IsInfix</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:Access" class="def">Access</a> <a href="src/Agda-Syntax-Common.html#Access" class="link">Source</a></p><div class="doc"><p>Access modifier.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:PrivateAccess" class="def">PrivateAccess</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:PublicAccess" class="def">PublicAccess</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:OnlyQualified" class="def">OnlyQualified</a></td><td class="doc"><p>Visible from outside, but not exported when opening the module
Used for qualified constructors.
</p></td></tr></table></div><div class="subs instances"><p id="control.i:Access" class="caption collapser" onclick="toggleSection('i:Access')">Instances</p><div id="section.i:Access" 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-Common.html#t:Access">Access</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-Common.html#t:Access">Access</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-Common.html#t:Access">Access</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-Common.html#t:Access">Access</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-Common.html#t:Access">Access</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:IsAbstract" class="def">IsAbstract</a> <a href="src/Agda-Syntax-Common.html#IsAbstract" class="link">Source</a></p><div class="doc"><p>Abstract or concrete
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:AbstractDef" class="def">AbstractDef</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:ConcreteDef" class="def">ConcreteDef</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:IsAbstract" class="caption collapser" onclick="toggleSection('i:IsAbstract')">Instances</p><div id="section.i:IsAbstract" 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-Common.html#t:IsAbstract">IsAbstract</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-Common.html#t:IsAbstract">IsAbstract</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-Common.html#t:IsAbstract">IsAbstract</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-Common.html#t:IsAbstract">IsAbstract</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-Common.html#t:IsAbstract">IsAbstract</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:Nat" class="def">Nat</a> = <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a><a href="src/Agda-Syntax-Common.html#Nat" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Arity" class="def">Arity</a> = <a href="Agda-Syntax-Common.html#t:Nat">Nat</a><a href="src/Agda-Syntax-Common.html#Arity" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:NameId" class="def">NameId</a> <a href="src/Agda-Syntax-Common.html#NameId" class="link">Source</a></p><div class="doc"><p>The unique identifier of a name. Second argument is the top-level module
identifier.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NameId" class="def">NameId</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:NameId" class="caption collapser" onclick="toggleSection('i:NameId')">Instances</p><div id="section.i:NameId" class="show"><table><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-Common.html#t:NameId">NameId</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-Common.html#t:NameId">NameId</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-Common.html#t:NameId">NameId</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-Common.html#t:NameId">NameId</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-Common.html#t:NameId">NameId</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-Common.html#t:NameId">NameId</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-Common.html#t:NameId">NameId</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Utils-Fresh.html#t:HasFresh">HasFresh</a> <a href="Agda-Syntax-Common.html#t:NameId">NameId</a> <a href="Agda-TypeChecking-Monad-Base.html#t:FreshThings">FreshThings</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:Constr" class="def">Constr</a> a <a href="src/Agda-Syntax-Common.html#Constr" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Constr" class="def">Constr</a> a</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Constr" class="caption collapser" onclick="toggleSection('i:Constr')">Instances</p><div id="section.i:Constr" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> (<a href="Agda-Syntax-Common.html#t:Constr">Constr</a> <a href="Agda-Syntax-Abstract.html#t:Constructor">Constructor</a>) <a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a></td><td class="doc empty"> </td></tr></table></div></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>
