<!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.Translation.ConcreteToAbstract</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-Translation-ConcreteToAbstract.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Syntax-Translation-ConcreteToAbstract.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.Translation.ConcreteToAbstract</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Translation from <a href="Agda-Syntax-Concrete.html">Agda.Syntax.Concrete</a> to <a href="Agda-Syntax-Abstract.html">Agda.Syntax.Abstract</a>. Involves scope analysis,
figuring out infix operator precedences and tidying up definitions.
</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">class</span> <a href="#t:ToAbstract">ToAbstract</a> concrete abstract | concrete -> abstract <span class="keyword">where</span><ul class="subs"><li><a href="#v:toAbstract">toAbstract</a> :: concrete -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> abstract</li></ul></li><li class="src short"><a href="#v:localToAbstract">localToAbstract</a> :: <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => c -> (a -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> b) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> b</li><li class="src short"><a href="#v:concreteToAbstract_">concreteToAbstract_</a> :: <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => c -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a</li><li class="src short"><a href="#v:concreteToAbstract">concreteToAbstract</a> :: <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> c -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a</li><li class="src short"><span class="keyword">newtype</span> <a href="#t:NewModuleQName">NewModuleQName</a> = <a href="#v:NewModuleQName">NewModuleQName</a> <a href="Agda-Syntax-Concrete-Name.html#t:QName">QName</a></li><li class="src short"><span class="keyword">newtype</span> <a href="#t:OldName">OldName</a> = <a href="#v:OldName">OldName</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></li><li class="src short"><span class="keyword">newtype</span> <a href="#t:TopLevel">TopLevel</a> a = <a href="#v:TopLevel">TopLevel</a> a</li><li class="src short"><span class="keyword">data</span> <a href="#t:TopLevelInfo">TopLevelInfo</a> = <a href="#v:TopLevelInfo">TopLevelInfo</a> {<ul class="subs"><li><a href="#v:topLevelDecls">topLevelDecls</a> :: [<a href="Agda-Syntax-Abstract.html#t:Declaration">Declaration</a>]</li><li><a href="#v:outsideScope">outsideScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a></li><li><a href="#v:insideScope">insideScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a></li></ul>}</li><li class="src short"><a href="#v:topLevelModuleName">topLevelModuleName</a> :: <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:TopLevelInfo">TopLevelInfo</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:AbstractRHS">AbstractRHS</a> </li><li class="src short"><span class="keyword">data</span> <a href="#t:NewModuleName">NewModuleName</a> </li><li class="src short"><span class="keyword">data</span> <a href="#t:OldModuleName">OldModuleName</a> </li><li class="src short"><span class="keyword">data</span> <a href="#t:NewName">NewName</a> a</li><li class="src short"><span class="keyword">data</span> <a href="#t:OldQName">OldQName</a> </li><li class="src short"><span class="keyword">data</span> <a href="#t:LeftHandSide">LeftHandSide</a> </li><li class="src short"><span class="keyword">data</span> <a href="#t:RightHandSide">RightHandSide</a> </li><li class="src short"><span class="keyword">data</span> <a href="#t:PatName">PatName</a> </li><li class="src short"><span class="keyword">data</span> <a href="#t:APatName">APatName</a> </li><li class="src short"><span class="keyword">data</span> <a href="#t:LetDef">LetDef</a> </li><li class="src short"><span class="keyword">data</span> <a href="#t:LetDefs">LetDefs</a> </li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:ToAbstract" class="def">ToAbstract</a> concrete abstract | concrete -> abstract <span class="keyword">where</span><a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#ToAbstract" class="link">Source</a></p><div class="doc"><p>Things that can be translated to abstract syntax are instances of this
class.
</p></div><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:toAbstract" class="def">toAbstract</a> :: concrete -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> abstract<a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#toAbstract" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:ToAbstract" class="caption collapser" onclick="toggleSection('i:ToAbstract')">Instances</p><div id="section.i:ToAbstract" class="show"><table><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-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><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><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><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-Definitions.html#t:Clause">Clause</a> <a href="Agda-Syntax-Abstract.html#t:Clause">Clause</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-Definitions.html#t:NiceDeclaration">NiceDeclaration</a> <a href="Agda-Syntax-Abstract.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:LeftHandSide">LeftHandSide</a> <a href="Agda-Syntax-Abstract.html#t:LHS">LHS</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:AbstractRHS">AbstractRHS</a> <a href="Agda-Syntax-Abstract.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-Translation-ConcreteToAbstract.html#t:RightHandSide">RightHandSide</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-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> ConstrDecl <a href="Agda-Syntax-Abstract.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:OldModuleName">OldModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewModuleQName">NewModuleQName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewModuleName">NewModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:PatName">PatName</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:APatName">APatName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:OldName">OldName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:OldQName">OldQName</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:Pragma">Pragma</a> [<a href="Agda-Syntax-Abstract.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: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-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:LetDef">LetDef</a> [<a href="Agda-Syntax-Abstract.html#t:LetBinding">LetBinding</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:LetDefs">LetDefs</a> [<a href="Agda-Syntax-Abstract.html#t:LetBinding">LetBinding</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-Translation-ConcreteToAbstract.html#t:NewName">NewName</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>) <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewName">NewName</a> <a href="Agda-Syntax-Concrete.html#t:BoundName">BoundName</a>) <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> [c] [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><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> c) (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> c) (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-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><tr><td class="src">(<a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c1 a1, <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c2 a2) => <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (c1, c2) (a1, a2)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="Agda-Syntax-Common.html#t:Named">Named</a> name c) (<a href="Agda-Syntax-Common.html#t:Named">Named</a> name a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c1 a1, <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c2 a2, <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c3 a3) => <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (c1, c2, c3) (a1, a2, a3)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:localToAbstract" class="def">localToAbstract</a> :: <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => c -> (a -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> b) -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> b<a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#localToAbstract" class="link">Source</a></p><div class="doc"><p>This operation does not affect the scope, i.e. the original scope
is restored upon completion.
</p></div></div><div class="top"><p class="src"><a name="v:concreteToAbstract_" class="def">concreteToAbstract_</a> :: <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => c -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a<a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#concreteToAbstract_" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:concreteToAbstract" class="def">concreteToAbstract</a> :: <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> c a => <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a> -> c -> <a href="Agda-Syntax-Scope-Monad.html#t:ScopeM">ScopeM</a> a<a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#concreteToAbstract" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">newtype</span> <a name="t:NewModuleQName" class="def">NewModuleQName</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#NewModuleQName" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NewModuleQName" class="def">NewModuleQName</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:NewModuleQName" class="caption collapser" onclick="toggleSection('i:NewModuleQName')">Instances</p><div id="section.i:NewModuleQName" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewModuleQName">NewModuleQName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">newtype</span> <a name="t:OldName" class="def">OldName</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#OldName" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:OldName" class="def">OldName</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:OldName" class="caption collapser" onclick="toggleSection('i:OldName')">Instances</p><div id="section.i:OldName" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:OldName">OldName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">newtype</span> <a name="t:TopLevel" class="def">TopLevel</a> a <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#TopLevel" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:TopLevel" class="def">TopLevel</a> a</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:TopLevel" class="caption collapser" onclick="toggleSection('i:TopLevel')">Instances</p><div id="section.i:TopLevel" class="show"><table><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></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:TopLevelInfo" class="def">TopLevelInfo</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#TopLevelInfo" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:TopLevelInfo" class="def">TopLevelInfo</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:topLevelDecls" class="def">topLevelDecls</a> :: [<a href="Agda-Syntax-Abstract.html#t:Declaration">Declaration</a>]</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:outsideScope" class="def">outsideScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:insideScope" class="def">insideScope</a> :: <a href="Agda-Syntax-Scope-Base.html#t:ScopeInfo">ScopeInfo</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:TopLevelInfo" class="caption collapser" onclick="toggleSection('i:TopLevelInfo')">Instances</p><div id="section.i:TopLevelInfo" class="show"><table><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></table></div></div></div><div class="top"><p class="src"><a name="v:topLevelModuleName" class="def">topLevelModuleName</a> :: <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:TopLevelInfo">TopLevelInfo</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a><a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#topLevelModuleName" class="link">Source</a></p><div class="doc"><p>The top-level module name.
</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:AbstractRHS" class="def">AbstractRHS</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#AbstractRHS" class="link">Source</a></p><div class="subs instances"><p id="control.i:AbstractRHS" class="caption collapser" onclick="toggleSection('i:AbstractRHS')">Instances</p><div id="section.i:AbstractRHS" class="show"><table><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-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:AbstractRHS">AbstractRHS</a> <a href="Agda-Syntax-Abstract.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-Translation-ConcreteToAbstract.html#t:RightHandSide">RightHandSide</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:AbstractRHS">AbstractRHS</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:NewModuleName" class="def">NewModuleName</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#NewModuleName" class="link">Source</a></p><div class="subs instances"><p id="control.i:NewModuleName" class="caption collapser" onclick="toggleSection('i:NewModuleName')">Instances</p><div id="section.i:NewModuleName" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewModuleName">NewModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:OldModuleName" class="def">OldModuleName</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#OldModuleName" class="link">Source</a></p><div class="subs instances"><p id="control.i:OldModuleName" class="caption collapser" onclick="toggleSection('i:OldModuleName')">Instances</p><div id="section.i:OldModuleName" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:OldModuleName">OldModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:NewName" class="def">NewName</a> a <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#NewName" class="link">Source</a></p><div class="subs instances"><p id="control.i:NewName" class="caption collapser" onclick="toggleSection('i:NewName')">Instances</p><div id="section.i:NewName" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewName">NewName</a> <a href="Agda-Syntax-Concrete-Name.html#t:Name">Name</a>) <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> (<a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:NewName">NewName</a> <a href="Agda-Syntax-Concrete.html#t:BoundName">BoundName</a>) <a href="Agda-Syntax-Abstract-Name.html#t:Name">Name</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:OldQName" class="def">OldQName</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#OldQName" class="link">Source</a></p><div class="subs instances"><p id="control.i:OldQName" class="caption collapser" onclick="toggleSection('i:OldQName')">Instances</p><div id="section.i:OldQName" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:OldQName">OldQName</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:LeftHandSide" class="def">LeftHandSide</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#LeftHandSide" class="link">Source</a></p><div class="subs instances"><p id="control.i:LeftHandSide" class="caption collapser" onclick="toggleSection('i:LeftHandSide')">Instances</p><div id="section.i:LeftHandSide" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:LeftHandSide">LeftHandSide</a> <a href="Agda-Syntax-Abstract.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:RightHandSide" class="def">RightHandSide</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#RightHandSide" class="link">Source</a></p><div class="subs instances"><p id="control.i:RightHandSide" class="caption collapser" onclick="toggleSection('i:RightHandSide')">Instances</p><div id="section.i:RightHandSide" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:RightHandSide">RightHandSide</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:AbstractRHS">AbstractRHS</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:PatName" class="def">PatName</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#PatName" class="link">Source</a></p><div class="subs instances"><p id="control.i:PatName" class="caption collapser" onclick="toggleSection('i:PatName')">Instances</p><div id="section.i:PatName" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:PatName">PatName</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:APatName">APatName</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:APatName" class="def">APatName</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#APatName" class="link">Source</a></p><div class="subs instances"><p id="control.i:APatName" class="caption collapser" onclick="toggleSection('i:APatName')">Instances</p><div id="section.i:APatName" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:PatName">PatName</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:APatName">APatName</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:LetDef" class="def">LetDef</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#LetDef" class="link">Source</a></p><div class="subs instances"><p id="control.i:LetDef" class="caption collapser" onclick="toggleSection('i:LetDef')">Instances</p><div id="section.i:LetDef" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:LetDef">LetDef</a> [<a href="Agda-Syntax-Abstract.html#t:LetBinding">LetBinding</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:LetDefs" class="def">LetDefs</a> <a href="src/Agda-Syntax-Translation-ConcreteToAbstract.html#LetDefs" class="link">Source</a></p><div class="subs instances"><p id="control.i:LetDefs" class="caption collapser" onclick="toggleSection('i:LetDefs')">Instances</p><div id="section.i:LetDefs" class="show"><table><tr><td class="src"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:ToAbstract">ToAbstract</a> <a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:LetDefs">LetDefs</a> [<a href="Agda-Syntax-Abstract.html#t:LetBinding">LetBinding</a>]</td><td class="doc empty"> </td></tr></table></div></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
