<!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.Concrete</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-Concrete.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Syntax-Concrete.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.Concrete</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">Expressions
</a></li><li><a href="#g:2">Bindings
</a></li><li><a href="#g:3">Declarations
</a></li><li><a href="#g:4">Pattern tools
</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>The concrete syntax is a raw representation of the program text
without any desugaring at all. This is what the parser produces.
The idea is that if we figure out how to keep the concrete syntax
around, it can be printed exactly as the user wrote it.
</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:Expr">Expr</a> <ul class="subs"><li>= <a href="#v:Ident">Ident</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> </li><li>| <a href="#v:Lit">Lit</a> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> </li><li>| <a href="#v:QuestionMark">QuestionMark</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</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-Common.html#t:Nat">Nat</a>) </li><li>| <a href="#v:Underscore">Underscore</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>) </li><li>| <a href="#v:RawApp">RawApp</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>] </li><li>| <a href="#v:App">App</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> (<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>) </li><li>| <a href="#v:OpApp">OpApp</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> [<a href="Agda-Syntax-Concrete.html#t:OpApp">OpApp</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>] </li><li>| <a href="#v:WithApp">WithApp</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>] </li><li>| <a href="#v:HiddenArg">HiddenArg</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</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 href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>) </li><li>| <a href="#v:InstanceArg">InstanceArg</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</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 href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>) </li><li>| <a href="#v:Lam">Lam</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:AbsurdLam">AbsurdLam</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> </li><li>| <a href="#v:ExtendedLam">ExtendedLam</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [(<a href="Agda-Syntax-Concrete.html#t:LHS">LHS</a>, <a href="Agda-Syntax-Concrete.html#t:RHS">RHS</a>, <a href="Agda-Syntax-Concrete.html#t:WhereClause">WhereClause</a>)] </li><li>| <a href="#v:Fun">Fun</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:Pi">Pi</a> <a href="Agda-Syntax-Concrete.html#t:Telescope">Telescope</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:Set">Set</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> </li><li>| <a href="#v:Prop">Prop</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> </li><li>| <a href="#v:SetN">SetN</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a> </li><li>| <a href="#v:Rec">Rec</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [(<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>, <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)] </li><li>| <a href="#v:RecUpdate">RecUpdate</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> [(<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>, <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)] </li><li>| <a href="#v:Let">Let</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:Paren">Paren</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:Absurd">Absurd</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> </li><li>| <a href="#v:As">As</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:Dot">Dot</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:ETel">ETel</a> <a href="Agda-Syntax-Concrete.html#t:Telescope">Telescope</a> </li><li>| <a href="#v:QuoteGoal">QuoteGoal</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:Quote">Quote</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> </li><li>| <a href="#v:QuoteTerm">QuoteTerm</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> </li><li>| <a href="#v:Unquote">Unquote</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> </li><li>| <a href="#v:DontCare">DontCare</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:OpApp">OpApp</a> e<ul class="subs"><li>= <a href="#v:SyntaxBindingLambda">SyntaxBindingLambda</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</a>] e </li><li>| <a href="#v:Ordinary">Ordinary</a> e </li></ul></li><li class="src short"><a href="#v:fromOrdinary">fromOrdinary</a> :: e -> <a href="Agda-Syntax-Concrete.html#t:OpApp">OpApp</a> e -> e</li><li class="src short">module <a href="Agda-Syntax-Concrete-Name.html">Agda.Syntax.Concrete.Name</a></li><li class="src short"><a href="#v:appView">appView</a> :: <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> -> <a href="Agda-Syntax-Concrete.html#t:AppView">AppView</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:AppView">AppView</a> = <a href="#v:AppView">AppView</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>]</li><li class="src short"><span class="keyword">data</span> <a href="#t:LamBinding">LamBinding</a> <ul class="subs"><li>= <a href="#v:DomainFree">DomainFree</a> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> <a href="Agda-Syntax-Concrete.html#t:BoundName">BoundName</a> </li><li>| <a href="#v:DomainFull">DomainFull</a> <a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:TypedBindings">TypedBindings</a> = <a href="#v:TypedBindings">TypedBindings</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Concrete.html#t:TypedBinding">TypedBinding</a>)</li><li class="src short"><span class="keyword">data</span> <a href="#t:TypedBinding">TypedBinding</a> <ul class="subs"><li>= <a href="#v:TBind">TBind</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:BoundName">BoundName</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:TNoBind">TNoBind</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:BoundName">BoundName</a> = <a href="#v:BName">BName</a> {<ul class="subs"><li><a href="#v:boundName">boundName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></li><li><a href="#v:bnameFixity">bnameFixity</a> :: <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a></li></ul>}</li><li class="src short"><a href="#v:mkBoundName_">mkBoundName_</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Concrete.html#t:BoundName">BoundName</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:Telescope">Telescope</a> = [<a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</a>]</li><li class="src short"><span class="keyword">data</span> <a href="#t:Declaration">Declaration</a> <ul class="subs"><li>= <a href="#v:TypeSig">TypeSig</a> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:Field">Field</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>) </li><li>| <a href="#v:FunClause">FunClause</a> <a href="Agda-Syntax-Concrete.html#t:LHS">LHS</a> <a href="Agda-Syntax-Concrete.html#t:RHS">RHS</a> <a href="Agda-Syntax-Concrete.html#t:WhereClause">WhereClause</a> </li><li>| <a href="#v:DataSig">DataSig</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:Data">Data</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</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.html#t:Expr">Expr</a>) [<a href="Agda-Syntax-Concrete.html#t:Constructor">Constructor</a>] </li><li>| <a href="#v:RecordSig">RecordSig</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:Record">Record</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</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>) [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</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.html#t:Expr">Expr</a>) [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>] </li><li>| <a href="#v:Infix">Infix</a> <a href="Agda-Syntax-Fixity.html#t:Fixity">Fixity</a> [<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>] </li><li>| <a href="#v:Syntax">Syntax</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Notation.html#t:Notation">Notation</a> </li><li>| <a href="#v:PatternSyn">PatternSyn</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>] <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> </li><li>| <a href="#v:Mutual">Mutual</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>] </li><li>| <a href="#v:Abstract">Abstract</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>] </li><li>| <a href="#v:Private">Private</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>] </li><li>| <a href="#v:Postulate">Postulate</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:TypeSignature">TypeSignature</a>] </li><li>| <a href="#v:Primitive">Primitive</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:TypeSignature">TypeSignature</a>] </li><li>| <a href="#v:Open">Open</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a> </li><li>| <a href="#v:Import">Import</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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.html#t:AsName">AsName</a>) <a href="Agda-Syntax-Concrete.html#t:OpenShortHand">OpenShortHand</a> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a> </li><li>| <a href="#v:ModuleMacro">ModuleMacro</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete.html#t:ModuleApplication">ModuleApplication</a> <a href="Agda-Syntax-Concrete.html#t:OpenShortHand">OpenShortHand</a> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a> </li><li>| <a href="#v:Module">Module</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> [<a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</a>] [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>] </li><li>| <a href="#v:Pragma">Pragma</a> <a href="Agda-Syntax-Concrete.html#t:Pragma">Pragma</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:ModuleApplication">ModuleApplication</a> <ul class="subs"><li>= <a href="#v:SectionApp">SectionApp</a> <a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:RecordModuleIFS">RecordModuleIFS</a> <a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> </li></ul></li><li class="src short"><span class="keyword">type</span> <a href="#t:TypeSignature">TypeSignature</a> = <a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:Constructor">Constructor</a> = <a href="Agda-Syntax-Concrete.html#t:TypeSignature">TypeSignature</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:ImportDirective">ImportDirective</a> = <a href="#v:ImportDirective">ImportDirective</a> {<ul class="subs"><li><a href="#v:importDirRange">importDirRange</a> :: !<a href="Agda-Syntax-Position.html#t:Range">Range</a></li><li><a href="#v:usingOrHiding">usingOrHiding</a> :: <a href="Agda-Syntax-Concrete.html#t:UsingOrHiding">UsingOrHiding</a></li><li><a href="#v:renaming">renaming</a> :: [<a href="Agda-Syntax-Concrete.html#t:Renaming">Renaming</a>]</li><li><a href="#v:publicOpen">publicOpen</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:UsingOrHiding">UsingOrHiding</a> <ul class="subs"><li>= <a href="#v:Hiding">Hiding</a> [<a href="Agda-Syntax-Concrete.html#t:ImportedName">ImportedName</a>] </li><li>| <a href="#v:Using">Using</a> [<a href="Agda-Syntax-Concrete.html#t:ImportedName">ImportedName</a>] </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:ImportedName">ImportedName</a> <ul class="subs"><li>= <a href="#v:ImportedModule">ImportedModule</a> { <ul class="subs"><li><a href="#v:importedName">importedName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></li></ul> }</li><li>| <a href="#v:ImportedName">ImportedName</a> { <ul class="subs"><li><a href="#v:importedName">importedName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></li></ul> }</li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:Renaming">Renaming</a> = <a href="#v:Renaming">Renaming</a> {<ul class="subs"><li><a href="#v:renFrom">renFrom</a> :: <a href="Agda-Syntax-Concrete.html#t:ImportedName">ImportedName</a></li><li><a href="#v:renTo">renTo</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></li><li><a href="#v:renToRange">renToRange</a> :: <a href="Agda-Syntax-Position.html#t:Range">Range</a></li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:AsName">AsName</a> = <a href="#v:AsName">AsName</a> {<ul class="subs"><li><a href="#v:asName">asName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></li><li><a href="#v:asRange">asRange</a> :: <a href="Agda-Syntax-Position.html#t:Range">Range</a></li></ul>}</li><li class="src short"><a href="#v:defaultImportDir">defaultImportDir</a> :: <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:OpenShortHand">OpenShortHand</a> <ul class="subs"><li>= <a href="#v:DoOpen">DoOpen</a> </li><li>| <a href="#v:DontOpen">DontOpen</a> </li></ul></li><li class="src short"><span class="keyword">type</span> <a href="#t:RewriteEqn">RewriteEqn</a> = <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:WithExpr">WithExpr</a> = <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:LHS">LHS</a> <ul class="subs"><li>= <a href="#v:LHS">LHS</a> { <ul class="subs"><li><a href="#v:lhsOriginalPattern">lhsOriginalPattern</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a></li><li><a href="#v:lhsWithPattern">lhsWithPattern</a> :: [<a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</li><li><a href="#v:lhsRewriteEqn">lhsRewriteEqn</a> :: [<a href="Agda-Syntax-Concrete.html#t:RewriteEqn">RewriteEqn</a>]</li><li><a href="#v:lhsWithExpr">lhsWithExpr</a> :: [<a href="Agda-Syntax-Concrete.html#t:WithExpr">WithExpr</a>]</li></ul> }</li><li>| <a href="#v:Ellipsis">Ellipsis</a> <a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>] [<a href="Agda-Syntax-Concrete.html#t:RewriteEqn">RewriteEqn</a>] [<a href="Agda-Syntax-Concrete.html#t:WithExpr">WithExpr</a>] </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:Pattern">Pattern</a> <ul class="subs"><li>= <a href="#v:IdentP">IdentP</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> </li><li>| <a href="#v:AppP">AppP</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> (<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>) </li><li>| <a href="#v:RawAppP">RawAppP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>] </li><li>| <a href="#v:OpAppP">OpAppP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> [<a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>] </li><li>| <a href="#v:HiddenP">HiddenP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</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 href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>) </li><li>| <a href="#v:InstanceP">InstanceP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</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 href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>) </li><li>| <a href="#v:ParenP">ParenP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> </li><li>| <a href="#v:WildP">WildP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> </li><li>| <a href="#v:AbsurdP">AbsurdP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> </li><li>| <a href="#v:AsP">AsP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> </li><li>| <a href="#v:DotP">DotP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:LitP">LitP</a> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:LHSCore">LHSCore</a> <ul class="subs"><li>= <a href="#v:LHSHead">LHSHead</a> { <ul class="subs"><li><a href="#v:lhsDefName">lhsDefName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></li><li><a href="#v:lhsPats">lhsPats</a> :: [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</li></ul> }</li><li>| <a href="#v:LHSProj">LHSProj</a> { <ul class="subs"><li><a href="#v:lhsDestructor">lhsDestructor</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></li><li><a href="#v:lhsPatsLeft">lhsPatsLeft</a> :: [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</li><li><a href="#v:lhsFocus">lhsFocus</a> :: <a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:LHSCore">LHSCore</a></li><li><a href="#v:lhsPatsRight">lhsPatsRight</a> :: [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</li></ul> }</li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:RHS">RHS</a> <ul class="subs"><li>= <a href="#v:AbsurdRHS">AbsurdRHS</a> </li><li>| <a href="#v:RHS">RHS</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:WhereClause">WhereClause</a> <ul class="subs"><li>= <a href="#v:NoWhere">NoWhere</a> </li><li>| <a href="#v:AnyWhere">AnyWhere</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>] </li><li>| <a href="#v:SomeWhere">SomeWhere</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>] </li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:Pragma">Pragma</a> <ul class="subs"><li>= <a href="#v:OptionsPragma">OptionsPragma</a> !<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>] </li><li>| <a href="#v:BuiltinPragma">BuiltinPragma</a> !<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> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> </li><li>| <a href="#v:CompiledDataPragma">CompiledDataPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] </li><li>| <a href="#v:CompiledTypePragma">CompiledTypePragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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>| <a href="#v:CompiledPragma">CompiledPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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>| <a href="#v:CompiledEpicPragma">CompiledEpicPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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>| <a href="#v:CompiledJSPragma">CompiledJSPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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>| <a href="#v:StaticPragma">StaticPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> </li><li>| <a href="#v:ImportPragma">ImportPragma</a> !<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> </li><li>| <a href="#v:ImpossiblePragma">ImpossiblePragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> </li><li>| <a href="#v:EtaPragma">EtaPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> </li><li>| <a href="#v:NoTerminationCheckPragma">NoTerminationCheckPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> </li></ul></li><li class="src short"><span class="keyword">type</span> <a href="#t:Module">Module</a> = ([<a href="Agda-Syntax-Concrete.html#t:Pragma">Pragma</a>], [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>])</li><li class="src short"><span class="keyword">data</span> <a href="#t:ThingWithFixity">ThingWithFixity</a> x = <a href="#v:ThingWithFixity">ThingWithFixity</a> x <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a></li><li class="src short"><a href="#v:topLevelModuleName">topLevelModuleName</a> :: <a href="Agda-Syntax-Concrete.html#t:Module">Module</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a></li><li class="src short"><a href="#v:patternHead">patternHead</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</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></li><li class="src short"><a href="#v:patternNames">patternNames</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> [<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>]</li></ul></div><div id="interface"><h1 id="g:1">Expressions
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Expr" class="def">Expr</a> <a href="src/Agda-Syntax-Concrete.html#Expr" class="link">Source</a></p><div class="doc"><p>Concrete expressions. Should represent exactly what the user wrote.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Ident" class="def">Ident</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></td><td class="doc"><p>ex: <code>x</code>
</p></td></tr><tr><td class="src"><a name="v:Lit" class="def">Lit</a> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a></td><td class="doc"><p>ex: <code>1</code> or <code>"foo"</code>
</p></td></tr><tr><td class="src"><a name="v:QuestionMark" class="def">QuestionMark</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</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-Common.html#t:Nat">Nat</a>)</td><td class="doc"><p>ex: <code>?</code> or <code>{! ... !}</code>
</p></td></tr><tr><td class="src"><a name="v:Underscore" class="def">Underscore</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>)</td><td class="doc"><p>ex: <code>_</code> or <code>_A_5</code>
</p></td></tr><tr><td class="src"><a name="v:RawApp" class="def">RawApp</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>]</td><td class="doc"><p>before parsing operators
</p></td></tr><tr><td class="src"><a name="v:App" class="def">App</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> (<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)</td><td class="doc"><p>ex: <code>e e</code>, <code>e {e}</code>, or <code>e {x = e}</code>
</p></td></tr><tr><td class="src"><a name="v:OpApp" class="def">OpApp</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> [<a href="Agda-Syntax-Concrete.html#t:OpApp">OpApp</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>]</td><td class="doc"><p>ex: <code>e + e</code>
</p></td></tr><tr><td class="src"><a name="v:WithApp" class="def">WithApp</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>]</td><td class="doc"><p>ex: <code>e | e1 | .. | en</code>
</p></td></tr><tr><td class="src"><a name="v:HiddenArg" class="def">HiddenArg</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</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 href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)</td><td class="doc"><p>ex: <code>{e}</code> or <code>{x=e}</code>
</p></td></tr><tr><td class="src"><a name="v:InstanceArg" class="def">InstanceArg</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</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 href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)</td><td class="doc"><p>ex: <code>{{e}}</code> or <code>{{x=e}}</code>
</p></td></tr><tr><td class="src"><a name="v:Lam" class="def">Lam</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>ex: <code>\x {y} -> e</code> or <code>\(x:A){y:B} -> e</code>
</p></td></tr><tr><td class="src"><a name="v:AbsurdLam" class="def">AbsurdLam</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a></td><td class="doc"><p>ex: <code>\ ()</code>
</p></td></tr><tr><td class="src"><a name="v:ExtendedLam" class="def">ExtendedLam</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [(<a href="Agda-Syntax-Concrete.html#t:LHS">LHS</a>, <a href="Agda-Syntax-Concrete.html#t:RHS">RHS</a>, <a href="Agda-Syntax-Concrete.html#t:WhereClause">WhereClause</a>)]</td><td class="doc"><p>ex: <code>\ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }</code>
</p></td></tr><tr><td class="src"><a name="v:Fun" class="def">Fun</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>ex: <code>e -> e</code> or <code>.e -> e</code> (NYI: <code>{e} -> e</code>)
</p></td></tr><tr><td class="src"><a name="v:Pi" class="def">Pi</a> <a href="Agda-Syntax-Concrete.html#t:Telescope">Telescope</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>ex: <code>(xs:e) -> e</code> or <code>{xs:e} -> e</code>
</p></td></tr><tr><td class="src"><a name="v:Set" class="def">Set</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc"><p>ex: <code>Set</code>
</p></td></tr><tr><td class="src"><a name="v:Prop" class="def">Prop</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc"><p>ex: <code>Prop</code>
</p></td></tr><tr><td class="src"><a name="v:SetN" class="def">SetN</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Integer">Integer</a></td><td class="doc"><p>ex: <code>Set0, Set1, ..</code>
</p></td></tr><tr><td class="src"><a name="v:Rec" class="def">Rec</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [(<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>, <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)]</td><td class="doc"><p>ex: <code>record {x = a; y = b}</code>
</p></td></tr><tr><td class="src"><a name="v:RecUpdate" class="def">RecUpdate</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> [(<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>, <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)]</td><td class="doc"><p>ex: <code>record e {x = a; y = b}</code>
</p></td></tr><tr><td class="src"><a name="v:Let" class="def">Let</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>ex: <code>let Ds in e</code>
</p></td></tr><tr><td class="src"><a name="v:Paren" class="def">Paren</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>ex: <code>(e)</code>
</p></td></tr><tr><td class="src"><a name="v:Absurd" class="def">Absurd</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc"><p>ex: <code>()</code> or <code>{}</code>, only in patterns
</p></td></tr><tr><td class="src"><a name="v:As" class="def">As</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>ex: <code>x@p</code>, only in patterns
</p></td></tr><tr><td class="src"><a name="v:Dot" class="def">Dot</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>ex: <code>.p</code>, only in patterns
</p></td></tr><tr><td class="src"><a name="v:ETel" class="def">ETel</a> <a href="Agda-Syntax-Concrete.html#t:Telescope">Telescope</a></td><td class="doc"><p>only used for printing telescopes
</p></td></tr><tr><td class="src"><a name="v:QuoteGoal" class="def">QuoteGoal</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>ex: <code>quoteGoal x in e</code>
</p></td></tr><tr><td class="src"><a name="v:Quote" class="def">Quote</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc"><p>ex: <code>quote</code>, should be applied to a name
</p></td></tr><tr><td class="src"><a name="v:QuoteTerm" class="def">QuoteTerm</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc"><p>ex: <code>quoteTerm</code>, should be applied to a term
</p></td></tr><tr><td class="src"><a name="v:Unquote" class="def">Unquote</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc"><p>ex: <code>unquote</code>, should be applied to a term of type <code>Term</code>
</p></td></tr><tr><td class="src"><a name="v:DontCare" class="def">DontCare</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>to print irrelevant things
</p></td></tr></table></div><div class="subs instances"><p id="control.i:Expr" class="caption collapser" onclick="toggleSection('i:Expr')">Instances</p><div id="section.i:Expr" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</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-Concrete.html#t:Expr">Expr</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-Concrete.html#t:Expr">Expr</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-Concrete.html#t:Expr">Expr</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-Concrete.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Concrete-Operators-Parser.html#t:IsExpr">IsExpr</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</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.html#t:Expr">Expr</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</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-TypeChecking-Monad-Base.html#t:InteractionId">InteractionId</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</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-TypeChecking-Monad-Base.html#t:NamedMeta">NamedMeta</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</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-Concrete.html#t:Expr">Expr</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</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-Concrete.html#t:LHSCore">LHSCore</a> (<a href="Agda-Syntax-Abstract.html#t:LHSCore-39-">LHSCore'</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</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-Concrete.html#t:Pattern">Pattern</a> (<a href="Agda-Syntax-Abstract.html#t:Pattern-39-">Pattern'</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</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.html#t:RHS">RHS</a> (<a href="Agda-Syntax-Concrete.html#t:RHS">RHS</a>, [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>], [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>], [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</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-Concrete.html#t:OpApp">OpApp</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</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.html#t:Expr">Expr</a>)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> (<a href="Agda-Syntax-Concrete.html#t:OpApp">OpApp</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</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-Abstract.html#t:Pattern-39-">Pattern'</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>) (<a href="Agda-Syntax-Abstract.html#t:Pattern-39-">Pattern'</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</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-Abstract.html#t:LHSCore-39-">LHSCore'</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>) (<a href="Agda-Syntax-Abstract.html#t:LHSCore-39-">LHSCore'</a> <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</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:OpApp" class="def">OpApp</a> e <a href="src/Agda-Syntax-Concrete.html#OpApp" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:SyntaxBindingLambda" class="def">SyntaxBindingLambda</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</a>] e</td><td class="doc"><p>an abstraction inside a special syntax declaration (see Issue 358 why we introduce this).
</p></td></tr><tr><td class="src"><a name="v:Ordinary" class="def">Ordinary</a> e</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:OpApp" class="caption collapser" onclick="toggleSection('i:OpApp')">Instances</p><div id="section.i:OpApp" 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-Concrete.html#t:OpApp">OpApp</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-Concrete.html#t:OpApp">OpApp</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-Concrete.html#t:OpApp">OpApp</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> e => <a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> (<a href="Agda-Syntax-Concrete.html#t:OpApp">OpApp</a> e)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Position.html#t:HasRange">HasRange</a> e => <a href="Agda-Syntax-Position.html#t:HasRange">HasRange</a> (<a href="Agda-Syntax-Concrete.html#t:OpApp">OpApp</a> e)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> (<a href="Agda-Syntax-Concrete.html#t:OpApp">OpApp</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:fromOrdinary" class="def">fromOrdinary</a> :: e -> <a href="Agda-Syntax-Concrete.html#t:OpApp">OpApp</a> e -> e<a href="src/Agda-Syntax-Concrete.html#fromOrdinary" class="link">Source</a></p></div><div class="top"><p class="src">module <a href="Agda-Syntax-Concrete-Name.html">Agda.Syntax.Concrete.Name</a></p></div><div class="top"><p class="src"><a name="v:appView" class="def">appView</a> :: <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> -> <a href="Agda-Syntax-Concrete.html#t:AppView">AppView</a><a href="src/Agda-Syntax-Concrete.html#appView" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:AppView" class="def">AppView</a> <a href="src/Agda-Syntax-Concrete.html#AppView" class="link">Source</a></p><div class="doc"><p>The <code><a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></code> is not an application.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:AppView" class="def">AppView</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a> [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>]</td><td class="doc empty"> </td></tr></table></div></div><h1 id="g:2">Bindings
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:LamBinding" class="def">LamBinding</a> <a href="src/Agda-Syntax-Concrete.html#LamBinding" class="link">Source</a></p><div class="doc"><p>A lambda binding is either domain free or typed.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:DomainFree" class="def">DomainFree</a> <a href="Agda-Syntax-Common.html#t:Hiding">Hiding</a> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> <a href="Agda-Syntax-Concrete.html#t:BoundName">BoundName</a></td><td class="doc"><p>. <code>x</code> or <code>{x}</code> or <code>.x</code> or <code>.{x}</code> or <code>{.x}</code>
</p></td></tr><tr><td class="src"><a name="v:DomainFull" class="def">DomainFull</a> <a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</a></td><td class="doc"><p>. <code>(xs : e)</code> or <code>{xs : e}</code>
</p></td></tr></table></div><div class="subs instances"><p id="control.i:LamBinding" class="caption collapser" onclick="toggleSection('i:LamBinding')">Instances</p><div id="section.i:LamBinding" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</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-Concrete.html#t:LamBinding">LamBinding</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-Concrete.html#t:LamBinding">LamBinding</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-Concrete.html#t:LamBinding">LamBinding</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-Concrete.html#t:LamBinding">LamBinding</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> <a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</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.html#t:LamBinding">LamBinding</a> <a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</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-Concrete.html#t:LamBinding">LamBinding</a> <a href="Agda-Syntax-Abstract.html#t:LamBinding">LamBinding</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:TypedBindings" class="def">TypedBindings</a> <a href="src/Agda-Syntax-Concrete.html#TypedBindings" class="link">Source</a></p><div class="doc"><p>A sequence of typed bindings with hiding information. Appears in dependent
function spaces, typed lambdas, and telescopes.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:TypedBindings" class="def">TypedBindings</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Concrete.html#t:TypedBinding">TypedBinding</a>)</td><td class="doc"><p>. <code>(xs : e)</code> or <code>{xs : e}</code>
</p></td></tr></table></div><div class="subs instances"><p id="control.i:TypedBindings" class="caption collapser" onclick="toggleSection('i:TypedBindings')">Instances</p><div id="section.i:TypedBindings" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</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-Concrete.html#t:TypedBindings">TypedBindings</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-Concrete.html#t:TypedBindings">TypedBindings</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-Concrete.html#t:TypedBindings">TypedBindings</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-Concrete.html#t:TypedBindings">TypedBindings</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> <a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</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.html#t:TypedBindings">TypedBindings</a> <a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</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-Concrete.html#t:TypedBindings">TypedBindings</a> <a href="Agda-Syntax-Abstract.html#t:TypedBindings">TypedBindings</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:TypedBinding" class="def">TypedBinding</a> <a href="src/Agda-Syntax-Concrete.html#TypedBinding" class="link">Source</a></p><div class="doc"><p>A typed binding.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:TBind" class="def">TBind</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:BoundName">BoundName</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:TNoBind" class="def">TNoBind</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:TypedBinding" class="caption collapser" onclick="toggleSection('i:TypedBinding')">Instances</p><div id="section.i:TypedBinding" 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:Typeable">Typeable</a> <a href="Agda-Syntax-Concrete.html#t:TypedBinding">TypedBinding</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-Concrete.html#t:TypedBinding">TypedBinding</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-Concrete.html#t:TypedBinding">TypedBinding</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-Concrete.html#t:TypedBinding">TypedBinding</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> <a href="Agda-Syntax-Concrete.html#t:TypedBinding">TypedBinding</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.html#t:TypedBinding">TypedBinding</a> <a href="Agda-Syntax-Concrete.html#t:TypedBinding">TypedBinding</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-Concrete.html#t:TypedBinding">TypedBinding</a> <a href="Agda-Syntax-Abstract.html#t:TypedBinding">TypedBinding</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:BoundName" class="def">BoundName</a> <a href="src/Agda-Syntax-Concrete.html#BoundName" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:BName" class="def">BName</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:boundName" class="def">boundName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:bnameFixity" class="def">bnameFixity</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:BoundName" class="caption collapser" onclick="toggleSection('i:BoundName')">Instances</p><div id="section.i:BoundName" 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:Typeable">Typeable</a> <a href="Agda-Syntax-Concrete.html#t:BoundName">BoundName</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-Concrete.html#t:BoundName">BoundName</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-Concrete.html#t:BoundName">BoundName</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-Concrete.html#t:BoundName">BoundName</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></table></div></div></div><div class="top"><p class="src"><a name="v:mkBoundName_" class="def">mkBoundName_</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> -> <a href="Agda-Syntax-Concrete.html#t:BoundName">BoundName</a><a href="src/Agda-Syntax-Concrete.html#mkBoundName_" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Telescope" class="def">Telescope</a> = [<a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</a>]<a href="src/Agda-Syntax-Concrete.html#Telescope" class="link">Source</a></p><div class="doc"><p>A telescope is a sequence of typed bindings. Bound variables are in scope
in later types.
</p></div></div><h1 id="g:3">Declarations
</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Declaration" class="def">Declaration</a> <a href="src/Agda-Syntax-Concrete.html#Declaration" class="link">Source</a></p><div class="doc"><p>The representation type of a declaration. The comments indicate
which type in the intended family the constructor targets.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:TypeSig" class="def">TypeSig</a> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>Axioms and functions can be irrelevant.
</p></td></tr><tr><td class="src"><a name="v:Field" class="def">Field</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>)</td><td class="doc"><p>Record field, can be hidden and/or irrelevant.
</p></td></tr><tr><td class="src"><a name="v:FunClause" class="def">FunClause</a> <a href="Agda-Syntax-Concrete.html#t:LHS">LHS</a> <a href="Agda-Syntax-Concrete.html#t:RHS">RHS</a> <a href="Agda-Syntax-Concrete.html#t:WhereClause">WhereClause</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:DataSig" class="def">DataSig</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>lone data signature in mutual block
</p></td></tr><tr><td class="src"><a name="v:Data" class="def">Data</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</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.html#t:Expr">Expr</a>) [<a href="Agda-Syntax-Concrete.html#t:Constructor">Constructor</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:RecordSig" class="def">RecordSig</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><p>lone record signature in mutual block
</p></td></tr><tr><td class="src"><a name="v:Record" class="def">Record</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</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>) [<a href="Agda-Syntax-Concrete.html#t:LamBinding">LamBinding</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.html#t:Expr">Expr</a>) [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>]</td><td class="doc"><p>The optional name is a name for the record constructor.
</p></td></tr><tr><td class="src"><a name="v:Infix" class="def">Infix</a> <a href="Agda-Syntax-Fixity.html#t:Fixity">Fixity</a> [<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Syntax" class="def">Syntax</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Notation.html#t:Notation">Notation</a></td><td class="doc"><p>notation declaration for a name
</p></td></tr><tr><td class="src"><a name="v:PatternSyn" class="def">PatternSyn</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>] <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Mutual" class="def">Mutual</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Abstract" class="def">Abstract</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Private" class="def">Private</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Postulate" class="def">Postulate</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:TypeSignature">TypeSignature</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Primitive" class="def">Primitive</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:TypeSignature">TypeSignature</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Open" class="def">Open</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Import" class="def">Import</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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.html#t:AsName">AsName</a>) <a href="Agda-Syntax-Concrete.html#t:OpenShortHand">OpenShortHand</a> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:ModuleMacro" class="def">ModuleMacro</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete.html#t:ModuleApplication">ModuleApplication</a> <a href="Agda-Syntax-Concrete.html#t:OpenShortHand">OpenShortHand</a> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Module" class="def">Module</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> [<a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</a>] [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Pragma" class="def">Pragma</a> <a href="Agda-Syntax-Concrete.html#t:Pragma">Pragma</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Declaration" class="caption collapser" onclick="toggleSection('i:Declaration')">Instances</p><div id="section.i:Declaration" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</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-Concrete.html#t:Declaration">Declaration</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-Concrete.html#t:Declaration">Declaration</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-Concrete.html#t:Declaration">Declaration</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-Concrete.html#t:Declaration">Declaration</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> <a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</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.html#t:Clause">Clause</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</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.html#t:LetBinding">LetBinding</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</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.html#t:Declaration">Declaration</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</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.html#t:RHS">RHS</a> (<a href="Agda-Syntax-Concrete.html#t:RHS">RHS</a>, [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>], [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>], [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</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-Concrete.html#t:Declaration">Declaration</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-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><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:TopLevel">TopLevel</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>]) <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:TopLevelInfo">TopLevelInfo</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-Concrete.html#t:Declaration">Declaration</a>] [<a href="Agda-Syntax-Abstract.html#t:Declaration">Declaration</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:ModuleApplication" class="def">ModuleApplication</a> <a href="src/Agda-Syntax-Concrete.html#ModuleApplication" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:SectionApp" class="def">SectionApp</a> <a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:TypedBindings">TypedBindings</a>] <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:RecordModuleIFS" class="def">RecordModuleIFS</a> <a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:ModuleApplication" class="caption collapser" onclick="toggleSection('i:ModuleApplication')">Instances</p><div id="section.i:ModuleApplication" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:ModuleApplication">ModuleApplication</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-Concrete.html#t:ModuleApplication">ModuleApplication</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-Concrete.html#t:ModuleApplication">ModuleApplication</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-Concrete.html#t:ModuleApplication">ModuleApplication</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-Concrete.html#t:ModuleApplication">ModuleApplication</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> <a href="Agda-Syntax-Concrete.html#t:ModuleApplication">ModuleApplication</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.html#t:ModuleApplication">ModuleApplication</a> <a href="Agda-Syntax-Concrete.html#t:ModuleApplication">ModuleApplication</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:TypeSignature" class="def">TypeSignature</a> = <a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a><a href="src/Agda-Syntax-Concrete.html#TypeSignature" class="link">Source</a></p><div class="doc"><p>Just type signatures.
</p></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Constructor" class="def">Constructor</a> = <a href="Agda-Syntax-Concrete.html#t:TypeSignature">TypeSignature</a><a href="src/Agda-Syntax-Concrete.html#Constructor" class="link">Source</a></p><div class="doc"><p>A data constructor declaration is just a type signature.
</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:ImportDirective" class="def">ImportDirective</a> <a href="src/Agda-Syntax-Concrete.html#ImportDirective" class="link">Source</a></p><div class="doc"><p>The things you are allowed to say when you shuffle names between name
spaces (i.e. in <code>import</code>, <code>namespace</code>, or <code>open</code> declarations).
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:ImportDirective" class="def">ImportDirective</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:importDirRange" class="def">importDirRange</a> :: !<a href="Agda-Syntax-Position.html#t:Range">Range</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:usingOrHiding" class="def">usingOrHiding</a> :: <a href="Agda-Syntax-Concrete.html#t:UsingOrHiding">UsingOrHiding</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:renaming" class="def">renaming</a> :: [<a href="Agda-Syntax-Concrete.html#t:Renaming">Renaming</a>]</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:publicOpen" class="def">publicOpen</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc"><p>Only for <code>open</code>. Exports the opened names from the current module.
</p></dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:ImportDirective" class="caption collapser" onclick="toggleSection('i:ImportDirective')">Instances</p><div id="section.i:ImportDirective" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</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-Concrete.html#t:ImportDirective">ImportDirective</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-Concrete.html#t:ImportDirective">ImportDirective</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-Concrete.html#t:ImportDirective">ImportDirective</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-Concrete.html#t:ImportDirective">ImportDirective</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:UsingOrHiding" class="def">UsingOrHiding</a> <a href="src/Agda-Syntax-Concrete.html#UsingOrHiding" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Hiding" class="def">Hiding</a> [<a href="Agda-Syntax-Concrete.html#t:ImportedName">ImportedName</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Using" class="def">Using</a> [<a href="Agda-Syntax-Concrete.html#t:ImportedName">ImportedName</a>]</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:UsingOrHiding" class="caption collapser" onclick="toggleSection('i:UsingOrHiding')">Instances</p><div id="section.i:UsingOrHiding" 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:Typeable">Typeable</a> <a href="Agda-Syntax-Concrete.html#t:UsingOrHiding">UsingOrHiding</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-Concrete.html#t:UsingOrHiding">UsingOrHiding</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-Concrete.html#t:UsingOrHiding">UsingOrHiding</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-Concrete.html#t:UsingOrHiding">UsingOrHiding</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:ImportedName" class="def">ImportedName</a> <a href="src/Agda-Syntax-Concrete.html#ImportedName" class="link">Source</a></p><div class="doc"><p>An imported name can be a module or a defined name
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:ImportedModule" class="def">ImportedModule</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:importedName" class="def">importedName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr><tr><td class="src"><a name="v:ImportedName" class="def">ImportedName</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:importedName" class="def">importedName</a> :: <a href="Agda-Syntax-Concrete-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:ImportedName" class="caption collapser" onclick="toggleSection('i:ImportedName')">Instances</p><div id="section.i:ImportedName" 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-Concrete.html#t:ImportedName">ImportedName</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-Concrete.html#t:ImportedName">ImportedName</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-Concrete.html#t:ImportedName">ImportedName</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-Concrete.html#t:ImportedName">ImportedName</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-Concrete.html#t:ImportedName">ImportedName</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-Concrete.html#t:ImportedName">ImportedName</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-Concrete.html#t:ImportedName">ImportedName</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:Renaming" class="def">Renaming</a> <a href="src/Agda-Syntax-Concrete.html#Renaming" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Renaming" class="def">Renaming</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:renFrom" class="def">renFrom</a> :: <a href="Agda-Syntax-Concrete.html#t:ImportedName">ImportedName</a></dt><dd class="doc"><p>Rename from this name.
</p></dd><dt class="src"><a name="v:renTo" class="def">renTo</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></dt><dd class="doc"><p>To this one.
</p></dd><dt class="src"><a name="v:renToRange" class="def">renToRange</a> :: <a href="Agda-Syntax-Position.html#t:Range">Range</a></dt><dd class="doc"><p>The range of the "to" keyword. Retained
for highlighting purposes.
</p></dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Renaming" class="caption collapser" onclick="toggleSection('i:Renaming')">Instances</p><div id="section.i:Renaming" 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:Typeable">Typeable</a> <a href="Agda-Syntax-Concrete.html#t:Renaming">Renaming</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-Concrete.html#t:Renaming">Renaming</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-Concrete.html#t:Renaming">Renaming</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:AsName" class="def">AsName</a> <a href="src/Agda-Syntax-Concrete.html#AsName" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:AsName" class="def">AsName</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:asName" class="def">asName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></dt><dd class="doc"><p>The "as" name.
</p></dd><dt class="src"><a name="v:asRange" class="def">asRange</a> :: <a href="Agda-Syntax-Position.html#t:Range">Range</a></dt><dd class="doc"><p>The range of the "as" keyword. Retained
for highlighting purposes.
</p></dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:AsName" class="caption collapser" onclick="toggleSection('i:AsName')">Instances</p><div id="section.i:AsName" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:AsName">AsName</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-Concrete.html#t:AsName">AsName</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-Concrete.html#t:AsName">AsName</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-Concrete.html#t:AsName">AsName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:defaultImportDir" class="def">defaultImportDir</a> :: <a href="Agda-Syntax-Concrete.html#t:ImportDirective">ImportDirective</a><a href="src/Agda-Syntax-Concrete.html#defaultImportDir" class="link">Source</a></p><div class="doc"><p>Default is directive is <code>private</code> (use everything, but do not export).
</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:OpenShortHand" class="def">OpenShortHand</a> <a href="src/Agda-Syntax-Concrete.html#OpenShortHand" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:DoOpen" class="def">DoOpen</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:DontOpen" class="def">DontOpen</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:OpenShortHand" class="caption collapser" onclick="toggleSection('i:OpenShortHand')">Instances</p><div id="section.i:OpenShortHand" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:OpenShortHand">OpenShortHand</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-Concrete.html#t:OpenShortHand">OpenShortHand</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-Concrete.html#t:OpenShortHand">OpenShortHand</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:RewriteEqn" class="def">RewriteEqn</a> = <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a><a href="src/Agda-Syntax-Concrete.html#RewriteEqn" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:WithExpr" class="def">WithExpr</a> = <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a><a href="src/Agda-Syntax-Concrete.html#WithExpr" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:LHS" class="def">LHS</a> <a href="src/Agda-Syntax-Concrete.html#LHS" class="link">Source</a></p><div class="doc"><p>Left hand sides can be written in infix style. For example:
</p><pre> n + suc m = suc (n + m)
(f ∘ g) x = f (g x)
</pre><p>We use fixity information to see which name is actually defined.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:LHS" class="def">LHS</a></td><td class="doc"><p>original pattern, with-patterns, rewrite equations and with-expressions
</p></td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:lhsOriginalPattern" class="def">lhsOriginalPattern</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a></dt><dd class="doc"><pre>f ps</pre></dd><dt class="src"><a name="v:lhsWithPattern" class="def">lhsWithPattern</a> :: [<a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</dt><dd class="doc"><p><code>| p</code> (many)
</p></dd><dt class="src"><a name="v:lhsRewriteEqn" class="def">lhsRewriteEqn</a> :: [<a href="Agda-Syntax-Concrete.html#t:RewriteEqn">RewriteEqn</a>]</dt><dd class="doc"><p><code>rewrite e</code> (many)
</p></dd><dt class="src"><a name="v:lhsWithExpr" class="def">lhsWithExpr</a> :: [<a href="Agda-Syntax-Concrete.html#t:WithExpr">WithExpr</a>]</dt><dd class="doc"><p><code>with e</code> (many)
</p></dd></dl><div class="clear"></div></div></td></tr><tr><td class="src"><a name="v:Ellipsis" class="def">Ellipsis</a> <a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>] [<a href="Agda-Syntax-Concrete.html#t:RewriteEqn">RewriteEqn</a>] [<a href="Agda-Syntax-Concrete.html#t:WithExpr">WithExpr</a>]</td><td class="doc"><p>new with-patterns, rewrite equations and with-expressions
</p></td></tr></table></div><div class="subs instances"><p id="control.i:LHS" class="caption collapser" onclick="toggleSection('i:LHS')">Instances</p><div id="section.i:LHS" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:LHS">LHS</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-Concrete.html#t:LHS">LHS</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-Concrete.html#t:LHS">LHS</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-Concrete.html#t:LHS">LHS</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-Concrete.html#t:LHS">LHS</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.html#t:LHS">LHS</a> <a href="Agda-Syntax-Concrete.html#t:LHS">LHS</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:Pattern" class="def">Pattern</a> <a href="src/Agda-Syntax-Concrete.html#Pattern" class="link">Source</a></p><div class="doc"><p>Concrete patterns. No literals in patterns at the moment.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:IdentP" class="def">IdentP</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></td><td class="doc"><p><code>c</code> or <code>x</code>
</p></td></tr><tr><td class="src"><a name="v:AppP" class="def">AppP</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> (<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>)</td><td class="doc"><p><code>p p'</code> or <code>p {x = p'}</code>
</p></td></tr><tr><td class="src"><a name="v:RawAppP" class="def">RawAppP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> [<a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</td><td class="doc"><p><code>p1..pn</code> before parsing operators
</p></td></tr><tr><td class="src"><a name="v:OpAppP" class="def">OpAppP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a> [<a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</td><td class="doc"><p>eg: <code>p => p'</code> for operator <code>_=>_</code>
</p></td></tr><tr><td class="src"><a name="v:HiddenP" class="def">HiddenP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</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 href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>)</td><td class="doc"><p><code>{p}</code> or <code>{x = p}</code>
</p></td></tr><tr><td class="src"><a name="v:InstanceP" class="def">InstanceP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</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 href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>)</td><td class="doc"><p><code>{{p}}</code> or <code>{{x = p}}</code>
</p></td></tr><tr><td class="src"><a name="v:ParenP" class="def">ParenP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a></td><td class="doc"><pre>(p)</pre></td></tr><tr><td class="src"><a name="v:WildP" class="def">WildP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc"><pre>_</pre></td></tr><tr><td class="src"><a name="v:AbsurdP" class="def">AbsurdP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc"><pre>()</pre></td></tr><tr><td class="src"><a name="v:AsP" class="def">AsP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a></td><td class="doc"><p><code>x@p</code> unused
</p></td></tr><tr><td class="src"><a name="v:DotP" class="def">DotP</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc"><pre>.e</pre></td></tr><tr><td class="src"><a name="v:LitP" class="def">LitP</a> <a href="Agda-Syntax-Literal.html#t:Literal">Literal</a></td><td class="doc"><p><code>0</code>, <code>1</code>, etc.
</p></td></tr></table></div><div class="subs instances"><p id="control.i:Pattern" class="caption collapser" onclick="toggleSection('i:Pattern')">Instances</p><div id="section.i:Pattern" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</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-Concrete.html#t:Pattern">Pattern</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-Concrete.html#t:Pattern">Pattern</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-Concrete.html#t:Pattern">Pattern</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-Concrete.html#t:Pattern">Pattern</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Concrete-Operators-Parser.html#t:IsExpr">IsExpr</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</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.html#t:Pattern">Pattern</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</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.html#t:LHSCore">LHSCore</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</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-Concrete.html#t:Pattern">Pattern</a> (<a href="Agda-Syntax-Abstract.html#t:Pattern-39-">Pattern'</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</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-Concrete.html#t:Pattern">Pattern</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:LHSCore" class="def">LHSCore</a> <a href="src/Agda-Syntax-Concrete.html#LHSCore" class="link">Source</a></p><div class="doc"><p>Processed (scope-checked) intermediate form of the core <code>f ps</code> of <code><a href="Agda-Syntax-Concrete.html#t:LHS">LHS</a></code>.
Corresponds to <code><a href="Agda-Syntax-Concrete.html#v:lhsOriginalPattern">lhsOriginalPattern</a></code>.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:LHSHead" class="def">LHSHead</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:lhsDefName" class="def">lhsDefName</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></dt><dd class="doc"><pre>f</pre></dd><dt class="src"><a name="v:lhsPats" class="def">lhsPats</a> :: [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</dt><dd class="doc"><pre>ps</pre></dd></dl><div class="clear"></div></div></td></tr><tr><td class="src"><a name="v:LHSProj" class="def">LHSProj</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:lhsDestructor" class="def">lhsDestructor</a> :: <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></dt><dd class="doc"><p>record projection identifier
</p></dd><dt class="src"><a name="v:lhsPatsLeft" class="def">lhsPatsLeft</a> :: [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</dt><dd class="doc"><p>side patterns
</p></dd><dt class="src"><a name="v:lhsFocus" class="def">lhsFocus</a> :: <a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:LHSCore">LHSCore</a></dt><dd class="doc"><p>main branch
</p></dd><dt class="src"><a name="v:lhsPatsRight" class="def">lhsPatsRight</a> :: [<a href="Agda-Syntax-Common.html#t:NamedArg">NamedArg</a> <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a>]</dt><dd class="doc"><p>side patterns
</p></dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:LHSCore" class="caption collapser" onclick="toggleSection('i:LHSCore')">Instances</p><div id="section.i:LHSCore" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:LHSCore">LHSCore</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-Concrete.html#t:LHSCore">LHSCore</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-Concrete.html#t:LHSCore">LHSCore</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-Concrete.html#t:LHSCore">LHSCore</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-Concrete.html#t:LHSCore">LHSCore</a> (<a href="Agda-Syntax-Abstract.html#t:LHSCore-39-">LHSCore'</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</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:RHS" class="def">RHS</a> <a href="src/Agda-Syntax-Concrete.html#RHS" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:AbsurdRHS" class="def">AbsurdRHS</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:RHS" class="def">RHS</a> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:RHS" class="caption collapser" onclick="toggleSection('i:RHS')">Instances</p><div id="section.i:RHS" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:RHS">RHS</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-Concrete.html#t:RHS">RHS</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-Concrete.html#t:RHS">RHS</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-Concrete.html#t:RHS">RHS</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-Concrete.html#t:RHS">RHS</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> <a href="Agda-Syntax-Concrete.html#t:RHS">RHS</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-Concrete.html#t:RHS">RHS</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:AbstractRHS">AbstractRHS</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.html#t:RHS">RHS</a> (<a href="Agda-Syntax-Concrete.html#t:RHS">RHS</a>, [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>], [<a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a>], [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</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:WhereClause" class="def">WhereClause</a> <a href="src/Agda-Syntax-Concrete.html#WhereClause" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NoWhere" class="def">NoWhere</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:AnyWhere" class="def">AnyWhere</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:SomeWhere" class="def">SomeWhere</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a> [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>]</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:WhereClause" class="caption collapser" onclick="toggleSection('i:WhereClause')">Instances</p><div id="section.i:WhereClause" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:WhereClause">WhereClause</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-Concrete.html#t:WhereClause">WhereClause</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-Concrete.html#t:WhereClause">WhereClause</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-Concrete.html#t:WhereClause">WhereClause</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-Concrete.html#t:WhereClause">WhereClause</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">LowerMeta</a> <a href="Agda-Syntax-Concrete.html#t:WhereClause">WhereClause</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:ToConcrete">ToConcrete</a> AsWhereDecls <a href="Agda-Syntax-Concrete.html#t:WhereClause">WhereClause</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:Pragma" class="def">Pragma</a> <a href="src/Agda-Syntax-Concrete.html#Pragma" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:OptionsPragma" class="def">OptionsPragma</a> !<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>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:BuiltinPragma" class="def">BuiltinPragma</a> !<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> <a href="Agda-Syntax-Concrete.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CompiledDataPragma" class="def">CompiledDataPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CompiledTypePragma" class="def">CompiledTypePragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CompiledPragma" class="def">CompiledPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CompiledEpicPragma" class="def">CompiledEpicPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CompiledJSPragma" class="def">CompiledJSPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-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></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:StaticPragma" class="def">StaticPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:ImportPragma" class="def">ImportPragma</a> !<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></td><td class="doc"><p>Invariant: The string must be a valid Haskell
module name.
</p></td></tr><tr><td class="src"><a name="v:ImpossiblePragma" class="def">ImpossiblePragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:EtaPragma" class="def">EtaPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:NoTerminationCheckPragma" class="def">NoTerminationCheckPragma</a> !<a href="Agda-Syntax-Position.html#t:Range">Range</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Pragma" class="caption collapser" onclick="toggleSection('i:Pragma')">Instances</p><div id="section.i:Pragma" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Syntax-Concrete.html#t:Pragma">Pragma</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-Concrete.html#t:Pragma">Pragma</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-Concrete.html#t:Pragma">Pragma</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-Concrete.html#t:Pragma">Pragma</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-Concrete.html#t:Pragma">Pragma</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-Translation-AbstractToConcrete.html#t:RangeAndPragma">RangeAndPragma</a> <a href="Agda-Syntax-Concrete.html#t:Pragma">Pragma</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-Concrete.html#t:Pragma">Pragma</a> [<a href="Agda-Syntax-Abstract.html#t:Pragma">Pragma</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:Module" class="def">Module</a> = ([<a href="Agda-Syntax-Concrete.html#t:Pragma">Pragma</a>], [<a href="Agda-Syntax-Concrete.html#t:Declaration">Declaration</a>])<a href="src/Agda-Syntax-Concrete.html#Module" class="link">Source</a></p><div class="doc"><p>Modules: Top-level pragmas plus other top-level declarations.
</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:ThingWithFixity" class="def">ThingWithFixity</a> x <a href="src/Agda-Syntax-Fixity.html#ThingWithFixity" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:ThingWithFixity" class="def">ThingWithFixity</a> x <a href="Agda-Syntax-Fixity.html#t:Fixity-39-">Fixity'</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:ThingWithFixity" class="caption collapser" onclick="toggleSection('i:ThingWithFixity')">Instances</p><div id="section.i:ThingWithFixity" 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-Concrete.html#t:ThingWithFixity">ThingWithFixity</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-Concrete.html#t:ThingWithFixity">ThingWithFixity</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-Concrete.html#t:ThingWithFixity">ThingWithFixity</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-Concrete.html#t:ThingWithFixity">ThingWithFixity</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> x => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> (<a href="Agda-Syntax-Concrete.html#t:ThingWithFixity">ThingWithFixity</a> x)</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-Concrete.html#t:ThingWithFixity">ThingWithFixity</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-Position.html#t:KillRange">KillRange</a> x => <a href="Agda-Syntax-Position.html#t:KillRange">KillRange</a> (<a href="Agda-Syntax-Concrete.html#t:ThingWithFixity">ThingWithFixity</a> x)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:topLevelModuleName" class="def">topLevelModuleName</a> :: <a href="Agda-Syntax-Concrete.html#t:Module">Module</a> -> <a href="Agda-Syntax-Concrete-Name.html#t:TopLevelModuleName">TopLevelModuleName</a><a href="src/Agda-Syntax-Concrete.html#topLevelModuleName" class="link">Source</a></p><div class="doc"><p>Computes the top-level module name.
</p><p>Precondition: The <code><a href="Agda-Syntax-Concrete.html#t:Module">Module</a></code> has to be well-formed.
</p></div></div><h1 id="g:4">Pattern tools
</h1><div class="top"><p class="src"><a name="v:patternHead" class="def">patternHead</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</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><a href="src/Agda-Syntax-Concrete.html#patternHead" class="link">Source</a></p><div class="doc"><p>Get the leftmost symbol in a pattern.
</p></div></div><div class="top"><p class="src"><a name="v:patternNames" class="def">patternNames</a> :: <a href="Agda-Syntax-Concrete.html#t:Pattern">Pattern</a> -> [<a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>]<a href="src/Agda-Syntax-Concrete.html#patternNames" class="link">Source</a></p><div class="doc"><p>Get all the identifiers in a pattern in left-to-right order.
</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>
