Sophie: ghc-Agda-devel-2.3.2.1-5.fc19 i686

ghc-Agda-devel-2.3.2.1-5.fc19.i686.rpm

<!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-2.3.2.1: A dependently typed functional programming language and proof assistant (Index - A)</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();};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><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="alphabet"><ul><li><a href="doc-index-A.html">A</a></li><li><a href="doc-index-B.html">B</a></li><li><a href="doc-index-C.html">C</a></li><li><a href="doc-index-D.html">D</a></li><li><a href="doc-index-E.html">E</a></li><li><a href="doc-index-F.html">F</a></li><li><a href="doc-index-G.html">G</a></li><li><a href="doc-index-H.html">H</a></li><li><a href="doc-index-I.html">I</a></li><li><a href="doc-index-J.html">J</a></li><li><a href="doc-index-K.html">K</a></li><li><a href="doc-index-L.html">L</a></li><li><a href="doc-index-M.html">M</a></li><li><a href="doc-index-N.html">N</a></li><li><a href="doc-index-O.html">O</a></li><li><a href="doc-index-P.html">P</a></li><li><a href="doc-index-Q.html">Q</a></li><li><a href="doc-index-R.html">R</a></li><li><a href="doc-index-S.html">S</a></li><li><a href="doc-index-T.html">T</a></li><li><a href="doc-index-U.html">U</a></li><li><a href="doc-index-V.html">V</a></li><li><a href="doc-index-W.html">W</a></li><li><a href="doc-index-X.html">X</a></li><li><a href="doc-index-Y.html">Y</a></li><li><a href="doc-index-Z.html">Z</a></li><li><a href="doc-index-58.html">:</a></li><li><a href="doc-index-33.html">!</a></li><li><a href="doc-index-36.html">$</a></li><li><a href="doc-index-38.html">&amp;</a></li><li><a href="doc-index-43.html">+</a></li><li><a href="doc-index-46.html">.</a></li><li><a href="doc-index-47.html">/</a></li><li><a href="doc-index-60.html">&lt;</a></li><li><a href="doc-index-61.html">=</a></li><li><a href="doc-index-62.html">&gt;</a></li><li><a href="doc-index-124.html">|</a></li><li><a href="doc-index-45.html">-</a></li><li><a href="doc-index-All.html">All</a></li></ul></div><div id="index"><p class="caption">Index - A</p><table><tr><td class="src">A</td><td class="module"><a href="Agda-Interaction-EmacsCommand.html#v:A">Agda.Interaction.EmacsCommand</a></td></tr><tr><td class="src">abort</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#v:abort">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">Abs</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Auto-Syntax.html#t:Abs">Agda.Auto.Syntax</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Auto-Syntax.html#v:Abs">Agda.Auto.Syntax</a></td></tr><tr><td class="alt">3 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Internal.html#t:Abs">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">4 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Abs">Agda.Syntax.Internal</a></td></tr><tr><td class="src">absApp</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:absApp">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">absAppHH</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:absAppHH">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">absBody</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:absBody">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">abslamvarname</td><td class="module"><a href="Agda-Auto-Convert.html#v:abslamvarname">Agda.Auto.Convert</a></td></tr><tr><td class="src">AbsModule</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:AbsModule">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">AbsName</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:AbsName">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">absName</td><td class="module"><a href="Agda-Syntax-Internal.html#v:absName">Agda.Syntax.Internal</a></td></tr><tr><td class="src">absolute</td><td class="module"><a href="Agda-Utils-FileName.html#v:absolute">Agda.Utils.FileName</a></td></tr><tr><td class="src">AbsolutePath</td><td class="module"><a href="Agda-Utils-FileName.html#t:AbsolutePath">Agda.Utils.FileName</a></td></tr><tr><td class="src">abspatvarname</td><td class="module"><a href="Agda-Auto-CaseSplit.html#v:abspatvarname">Agda.Auto.CaseSplit</a></td></tr><tr><td class="src">AbsToCon</td><td class="module"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:AbsToCon">Agda.Syntax.Translation.AbstractToConcrete</a></td></tr><tr><td class="src">Abstract</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Abstract">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#t:Abstract">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">abstract</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:abstract">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">abstractArgs</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:abstractArgs">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">AbstractDef</td><td class="module"><a href="Agda-Syntax-Common.html#v:AbstractDef">Agda.Syntax.Common</a></td></tr><tr><td class="src">AbstractMode</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:AbstractMode">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:AbstractMode">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">AbstractModule</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#t:AbstractModule">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">AbstractName</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#t:AbstractName">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">AbstractRHS</td><td class="module"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:AbstractRHS">Agda.Syntax.Translation.ConcreteToAbstract</a></td></tr><tr><td class="src">AbstractTerm</td><td class="module"><a href="Agda-TypeChecking-Abstract.html#t:AbstractTerm">Agda.TypeChecking.Abstract</a></td></tr><tr><td class="src">abstractTerm</td><td class="module"><a href="Agda-TypeChecking-Abstract.html#v:abstractTerm">Agda.TypeChecking.Abstract</a></td></tr><tr><td class="src">abstractToConcrete</td><td class="module"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#v:abstractToConcrete">Agda.Syntax.Translation.AbstractToConcrete</a></td></tr><tr><td class="src">abstractToConcreteCtx</td><td class="module"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#v:abstractToConcreteCtx">Agda.Syntax.Translation.AbstractToConcrete</a></td></tr><tr><td class="src">abstractToConcrete_</td><td class="module"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#v:abstractToConcrete_">Agda.Syntax.Translation.AbstractToConcrete</a></td></tr><tr><td class="src">Absurd</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Absurd">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">AbsurdLam</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:AbsurdLam">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:AbsurdLam">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">AbsurdLambda</td><td class="module"><a href="Agda-Auto-Syntax.html#v:AbsurdLambda">Agda.Auto.Syntax</a></td></tr><tr><td class="src">AbsurdP</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:AbsurdP">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:AbsurdP">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">AbsurdPatternRequiresNoRHS</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:AbsurdPatternRequiresNoRHS">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">AbsurdRHS</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:AbsurdRHS">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:AbsurdRHS">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">Access</td><td class="module"><a href="Agda-Syntax-Common.html#t:Access">Agda.Syntax.Common</a></td></tr><tr><td class="src">actOnMeta</td><td class="module"><a href="Agda-Interaction-CommandLine-CommandLine.html#v:actOnMeta">Agda.Interaction.CommandLine.CommandLine</a></td></tr><tr><td class="src">actualConstructor</td><td class="module"><a href="Agda-TypeChecking-Rules-Def.html#v:actualConstructor">Agda.TypeChecking.Rules.Def</a></td></tr><tr><td class="src">acyclic</td><td class="module"><a href="Agda-Utils-Graph.html#v:acyclic">Agda.Utils.Graph</a></td></tr><tr><td class="src">add</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Termination-Semiring.html#v:add">Agda.Termination.Semiring</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Termination-Matrix.html#v:add">Agda.Termination.Matrix</a></td></tr><tr><td class="alt">3 (Function)</td><td class="module"><a href="Agda-Termination-SparseMatrix.html#v:add">Agda.Termination.SparseMatrix</a></td></tr><tr><td class="src">addAwakeConstraints</td><td class="module"><a href="Agda-TypeChecking-Monad-Constraints.html#v:addAwakeConstraints">Agda.TypeChecking.Monad.Constraints</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addblk</td><td class="module"><a href="Agda-Auto-Typecheck.html#v:addblk">Agda.Auto.Typecheck</a></td></tr><tr><td class="src">addColumn</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Termination-Matrix.html#v:addColumn">Agda.Termination.Matrix</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Termination-SparseMatrix.html#v:addColumn">Agda.Termination.SparseMatrix</a></td></tr><tr><td class="src">addConnection</td><td class="module"><a href="Agda-Interaction-Highlighting-Dot.html#v:addConnection">Agda.Interaction.Highlighting.Dot</a></td></tr><tr><td class="src">addConstant</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:addConstant">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addConstraint</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Utils-Warshall.html#v:addConstraint">Agda.Utils.Warshall</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-TypeChecking-Constraints.html#v:addConstraint">Agda.TypeChecking.Constraints</a></td></tr><tr><td class="alt">3 (Function)</td><td class="module"><a href="Agda-Compiler-Epic-Injection.html#v:addConstraint">Agda.Compiler.Epic.Injection</a></td></tr><tr><td class="src">addConstraint'</td><td class="module"><a href="Agda-TypeChecking-Monad-Constraints.html#v:addConstraint-39-">Agda.TypeChecking.Monad.Constraints</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addContext</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:addContext">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addCtx</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:addCtx">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addCtxs</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:addCtxs">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addCtxString</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:addCtxString">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addCtxString_</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:addCtxString_">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addCtxTel</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:addCtxTel">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addDecl</td><td class="module"><a href="Agda-Interaction-BasicOps.html#v:addDecl">Agda.Interaction.BasicOps</a></td></tr><tr><td class="src">addDefName</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:addDefName">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">addDisplayForm</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:addDisplayForm">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addDisplayForms</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:addDisplayForms">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addEdge</td><td class="module"><a href="Agda-Utils-Warshall.html#v:addEdge">Agda.Utils.Warshall</a></td></tr><tr><td class="src">addend</td><td class="module"><a href="Agda-Auto-Typecheck.html#v:addend">Agda.Auto.Typecheck</a></td></tr><tr><td class="src">addEpicCode</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:addEpicCode">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addEquality</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:addEquality">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">addEqualityHH</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:addEqualityHH">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">addExtLambdaTele</td><td class="module"><a href="Agda-TypeChecking-Monad-State.html#v:addExtLambdaTele">Agda.TypeChecking.Monad.State</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">AddExtraRef</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:AddExtraRef">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">addFinalNewLine</td><td class="module"><a href="Agda-Utils-String.html#v:addFinalNewLine">Agda.Utils.String</a></td></tr><tr><td class="src">addFlex</td><td class="module"><a href="Agda-Utils-Warshall.html#v:addFlex">Agda.Utils.Warshall</a></td></tr><tr><td class="src">addForcingAnnotations</td><td class="module"><a href="Agda-TypeChecking-Forcing.html#v:addForcingAnnotations">Agda.TypeChecking.Forcing</a></td></tr><tr><td class="src">addHaskellCode</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:addHaskellCode">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addHaskellImport</td><td class="module"><a href="Agda-TypeChecking-Monad-State.html#v:addHaskellImport">Agda.TypeChecking.Monad.State</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addHaskellType</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:addHaskellType">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addImport</td><td class="module"><a href="Agda-TypeChecking-Monad-Imports.html#v:addImport">Agda.TypeChecking.Monad.Imports</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addImportCycleCheck</td><td class="module"><a href="Agda-TypeChecking-Monad-Imports.html#v:addImportCycleCheck">Agda.TypeChecking.Monad.Imports</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addImportedThings</td><td class="module"><a href="Agda-Interaction-Imports.html#v:addImportedThings">Agda.Interaction.Imports</a></td></tr><tr><td class="src">addInteractionPoint</td><td class="module"><a href="Agda-TypeChecking-Monad-MetaVars.html#v:addInteractionPoint">Agda.TypeChecking.Monad.MetaVars</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addJSCode</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:addJSCode">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addLetBinding</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:addLetBinding">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addModule</td><td class="module"><a href="Agda-Interaction-Highlighting-Dot.html#v:addModule">Agda.Interaction.Highlighting.Dot</a></td></tr><tr><td class="src">addModuleToScope</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:addModuleToScope">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">addNamesToScope</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:addNamesToScope">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">addNameToScope</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:addNameToScope">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">addNode</td><td class="module"><a href="Agda-Utils-Warshall.html#v:addNode">Agda.Utils.Warshall</a></td></tr><tr><td class="src">addRow</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Termination-Matrix.html#v:addRow">Agda.Termination.Matrix</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Termination-SparseMatrix.html#v:addRow">Agda.Termination.SparseMatrix</a></td></tr><tr><td class="src">addSection</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:addSection">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">addSuffix</td><td class="module"><a href="Agda-Utils-Suffix.html#v:addSuffix">Agda.Utils.Suffix</a></td></tr><tr><td class="src">addtrailingargs</td><td class="module"><a href="Agda-Auto-Syntax.html#v:addtrailingargs">Agda.Auto.Syntax</a></td></tr><tr><td class="src">ADef</td><td class="module"><a href="Agda-TypeChecking-Positivity.html#v:ADef">Agda.TypeChecking.Positivity</a></td></tr><tr><td class="src">AdjList</td><td class="module"><a href="Agda-Utils-Warshall.html#t:AdjList">Agda.Utils.Warshall</a></td></tr><tr><td class="src">adjust</td><td class="module">Agda.Utils.HashMap</td></tr><tr><td class="src">agdaTermType</td><td class="module"><a href="Agda-TypeChecking-Quote.html#v:agdaTermType">Agda.TypeChecking.Quote</a></td></tr><tr><td class="src">ALConPar</td><td class="module"><a href="Agda-Auto-Syntax.html#v:ALConPar">Agda.Auto.Syntax</a></td></tr><tr><td class="src">ALCons</td><td class="module"><a href="Agda-Auto-Syntax.html#v:ALCons">Agda.Auto.Syntax</a></td></tr><tr><td class="src">AlexEOF</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#v:AlexEOF">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">AlexError</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#v:AlexError">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">alexGetByte</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#v:alexGetByte">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="src">alexGetChar</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#v:alexGetChar">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="src">AlexInput</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#t:AlexInput">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#v:AlexInput">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="src">alexInputPrevChar</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#v:alexInputPrevChar">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="src">AlexReturn</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#t:AlexReturn">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">alexScanUser</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#v:alexScanUser">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">AlexSkip</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#v:AlexSkip">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">AlexToken</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#v:AlexToken">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">align</td><td class="module"><a href="Agda-Utils-Pretty.html#v:align">Agda.Utils.Pretty</a></td></tr><tr><td class="src">allEqual</td><td class="module"><a href="Agda-Utils-List.html#v:allEqual">Agda.Utils.List</a></td></tr><tr><td class="src">allHoles</td><td class="module"><a href="Agda-Syntax-Internal-Pattern.html#v:allHoles">Agda.Syntax.Internal.Pattern</a></td></tr><tr><td class="src">allHolesWithContents</td><td class="module"><a href="Agda-Syntax-Internal-Pattern.html#v:allHolesWithContents">Agda.Syntax.Internal.Pattern</a></td></tr><tr><td class="src">allKindsOfNames</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:allKindsOfNames">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">allMetaKinds</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:allMetaKinds">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">allMetas</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:allMetas">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">allNames</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:allNames">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">allNamesInScope</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:allNamesInScope">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">allNamesInScope'</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:allNamesInScope-39-">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">allowedVar</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#v:allowedVar">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">allPaths</td><td class="module"><a href="Agda-Utils-Graph.html#v:allPaths">Agda.Utils.Graph</a></td></tr><tr><td class="src">allRight</td><td class="module"><a href="Agda-Utils-Either.html#v:allRight">Agda.Utils.Either</a></td></tr><tr><td class="src">allThingsInScope</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:allThingsInScope">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">allVars</td><td class="module"><a href="Agda-TypeChecking-Free.html#v:allVars">Agda.TypeChecking.Free</a></td></tr><tr><td class="src">ALNil</td><td class="module"><a href="Agda-Auto-Syntax.html#v:ALNil">Agda.Auto.Syntax</a></td></tr><tr><td class="src">ALProj</td><td class="module"><a href="Agda-Auto-Syntax.html#v:ALProj">Agda.Auto.Syntax</a></td></tr><tr><td class="src">alreadyVisited</td><td class="module"><a href="Agda-Interaction-Imports.html#v:alreadyVisited">Agda.Interaction.Imports</a></td></tr><tr><td class="src">altM1</td><td class="module"><a href="Agda-Utils-Monad.html#v:altM1">Agda.Utils.Monad</a></td></tr><tr><td class="src">Ambiguous</td><td class="module"><a href="Agda-Interaction-FindFile.html#v:Ambiguous">Agda.Interaction.FindFile</a></td></tr><tr><td class="src">AmbiguousFunClauses</td><td class="module"><a href="Agda-Syntax-Concrete-Definitions.html#v:AmbiguousFunClauses">Agda.Syntax.Concrete.Definitions</a></td></tr><tr><td class="src">AmbiguousModule</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:AmbiguousModule">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">AmbiguousName</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:AmbiguousName">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">AmbiguousParseForApplication</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:AmbiguousParseForApplication">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">AmbiguousParseForLHS</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:AmbiguousParseForLHS">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">AmbiguousQName</td><td class="module"><a href="Agda-Syntax-Abstract-Name.html#t:AmbiguousQName">Agda.Syntax.Abstract.Name</a>, Agda.Syntax.Internal, Agda.Syntax.Abstract</td></tr><tr><td class="src">AmbiguousTopLevelModuleName</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:AmbiguousTopLevelModuleName">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">AmbQ</td><td class="module"><a href="Agda-Syntax-Abstract-Name.html#v:AmbQ">Agda.Syntax.Abstract.Name</a>, Agda.Syntax.Internal, Agda.Syntax.Abstract</td></tr><tr><td class="src">amodName</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:amodName">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">anameKind</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:anameKind">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">anameName</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:anameName">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">AnArg</td><td class="module"><a href="Agda-TypeChecking-Positivity.html#v:AnArg">Agda.TypeChecking.Positivity</a></td></tr><tr><td class="src">And</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:And">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">and2M</td><td class="module"><a href="Agda-Utils-Monad.html#v:and2M">Agda.Utils.Monad</a></td></tr><tr><td class="src">andM</td><td class="module"><a href="Agda-Utils-Monad.html#v:andM">Agda.Utils.Monad</a></td></tr><tr><td class="src">AnyAbstract</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:AnyAbstract">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">anyAbstract</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:anyAbstract">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">AnyWhere</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:AnyWhere">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">APatName</td><td class="module"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:APatName">Agda.Syntax.Translation.ConcreteToAbstract</a></td></tr><tr><td class="src">App</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Auto-Syntax.html#v:App">Agda.Auto.Syntax</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:App">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:App">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="alt">4 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:App">Agda.Syntax.Abstract</a></td></tr><tr><td class="alt">5 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-EtaContract.html#v:App">Agda.TypeChecking.EtaContract</a></td></tr><tr><td class="src">app</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:app">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">appBrackets</td><td class="module"><a href="Agda-Syntax-Fixity.html#v:appBrackets">Agda.Syntax.Fixity</a></td></tr><tr><td class="src">appDef</td><td class="module"><a href="Agda-TypeChecking-Reduce.html#v:appDef">Agda.TypeChecking.Reduce</a></td></tr><tr><td class="src">appDef'</td><td class="module"><a href="Agda-TypeChecking-Reduce.html#v:appDef-39-">Agda.TypeChecking.Reduce</a></td></tr><tr><td class="src">Application</td><td class="module"><a href="Agda-Syntax-Abstract-Views.html#v:Application">Agda.Syntax.Abstract.Views</a></td></tr><tr><td class="src">Apply</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:Apply">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Apply">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Apply">Agda.Syntax.Abstract</a></td></tr><tr><td class="alt">4 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#t:Apply">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">apply</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Substitution.html#v:apply">Agda.Compiler.JS.Substitution</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:apply">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">applyDroppingParameters</td><td class="module"><a href="Agda-TypeChecking-InstanceArguments.html#v:applyDroppingParameters">Agda.TypeChecking.InstanceArguments</a></td></tr><tr><td class="src">ApplyHH</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ApplyHH">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">applyHH</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:applyHH">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">applyImportDirective</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:applyImportDirective">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">applyImportDirectiveM</td><td class="module"><a href="Agda-Syntax-Scope-Monad.html#v:applyImportDirectiveM">Agda.Syntax.Scope.Monad</a></td></tr><tr><td class="src">applyperm</td><td class="module"><a href="Agda-Auto-CaseSplit.html#v:applyperm">Agda.Auto.CaseSplit</a></td></tr><tr><td class="src">applyRelevance</td><td class="module"><a href="Agda-TypeChecking-Irrelevance.html#v:applyRelevance">Agda.TypeChecking.Irrelevance</a></td></tr><tr><td class="src">applyRelevanceToContext</td><td class="module"><a href="Agda-TypeChecking-Irrelevance.html#v:applyRelevanceToContext">Agda.TypeChecking.Irrelevance</a></td></tr><tr><td class="src">applySection</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:applySection">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">applySubst</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:applySubst">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">AppP</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:AppP">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">appP</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:appP">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">apps</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:apps">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">AppV</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:AppV">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">AppView</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Concrete.html#t:AppView">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:AppView">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">3 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Abstract-Views.html#t:AppView">Agda.Syntax.Abstract.Views</a></td></tr><tr><td class="src">appView</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:appView">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Abstract-Views.html#v:appView">Agda.Syntax.Abstract.Views</a></td></tr><tr><td class="src">apTCMT</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:apTCMT">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">Arbitrary</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">arbitrary</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">arbitraryBoundedEnum</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">arbitraryBoundedIntegral</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">arbitraryBoundedRandom</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">arbitrarySizedBoundedIntegral</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">arbitrarySizedFractional</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">arbitrarySizedIntegral</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">Arc</td><td class="module"><a href="Agda-Utils-Warshall.html#v:Arc">Agda.Utils.Warshall</a></td></tr><tr><td class="src">Arg</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Common.html#t:Arg">Agda.Syntax.Common</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Common.html#v:Arg">Agda.Syntax.Common</a></td></tr><tr><td class="src">argFromDom</td><td class="module"><a href="Agda-Syntax-Common.html#v:argFromDom">Agda.Syntax.Common</a></td></tr><tr><td class="src">argH</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:argH">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">argHiding</td><td class="module"><a href="Agda-Syntax-Common.html#v:argHiding">Agda.Syntax.Common</a></td></tr><tr><td class="src">argIsDef</td><td class="module"><a href="Agda-Compiler-Epic-NatDetection.html#v:argIsDef">Agda.Compiler.Epic.NatDetection</a></td></tr><tr><td class="src">ArgList</td><td class="module"><a href="Agda-Auto-Syntax.html#t:ArgList">Agda.Auto.Syntax</a></td></tr><tr><td class="src">argN</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:argN">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">argName</td><td class="module"><a href="Agda-Syntax-Internal.html#v:argName">Agda.Syntax.Internal</a></td></tr><tr><td class="src">ArgNode</td><td class="module"><a href="Agda-TypeChecking-Positivity.html#v:ArgNode">Agda.TypeChecking.Positivity</a></td></tr><tr><td class="src">argpatts</td><td class="module"><a href="Agda-Compiler-MAlonzo-Compiler.html#v:argpatts">Agda.Compiler.MAlonzo.Compiler</a></td></tr><tr><td class="src">argRelevance</td><td class="module"><a href="Agda-Syntax-Common.html#v:argRelevance">Agda.Syntax.Common</a></td></tr><tr><td class="src">Args</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="alt">3 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Internal.html#t:Args">Agda.Syntax.Internal</a></td></tr><tr><td class="src">args</td><td class="module"><a href="Agda-Compiler-JS-Compiler.html#v:args">Agda.Compiler.JS.Compiler</a></td></tr><tr><td class="src">ArgumentCtx</td><td class="module"><a href="Agda-Syntax-Fixity.html#v:ArgumentCtx">Agda.Syntax.Fixity</a></td></tr><tr><td class="src">ArgumentTo</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:ArgumentTo">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">Arity</td><td class="module"><a href="Agda-Syntax-Common.html#t:Arity">Agda.Syntax.Common</a></td></tr><tr><td class="src">arity</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Internal.html#v:arity">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-TypeChecking-CompiledClause.html#v:arity">Agda.TypeChecking.CompiledClause</a></td></tr><tr><td class="src">arrow</td><td class="module"><a href="Agda-Syntax-Concrete-Pretty.html#v:arrow">Agda.Syntax.Concrete.Pretty</a></td></tr><tr><td class="src">As</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:As">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">AsB</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:AsB">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">AsBinding</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:AsBinding">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">AsIs</td><td class="module"><a href="Agda-Interaction-BasicOps.html#v:AsIs">Agda.Interaction.BasicOps</a></td></tr><tr><td class="src">askPostpone</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:askPostpone">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">AsName</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Concrete.html#t:AsName">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:AsName">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">asName</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:asName">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">AsP</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:AsP">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:AsP">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">Aspect</td><td class="module"><a href="Agda-Interaction-Highlighting-Precise.html#t:Aspect">Agda.Interaction.Highlighting.Precise</a></td></tr><tr><td class="src">aspect</td><td class="module"><a href="Agda-Interaction-Highlighting-Precise.html#v:aspect">Agda.Interaction.Highlighting.Precise</a></td></tr><tr><td class="src">asRange</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:asRange">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">Assign</td><td class="module"><a href="Agda-Interaction-BasicOps.html#v:Assign">Agda.Interaction.BasicOps</a></td></tr><tr><td class="src">assign</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:assign">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">assignConstrTag</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:assignConstrTag">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">assignConstrTag'</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:assignConstrTag-39-">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">assignTerm</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:assignTerm">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">assignTerm'</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:assignTerm-39-">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">assignV</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:assignV">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">associative</td><td class="module"><a href="Agda-Utils-TestHelpers.html#v:associative">Agda.Utils.TestHelpers</a></td></tr><tr><td class="src">asView</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Split.html#v:asView">Agda.TypeChecking.Rules.LHS.Split</a></td></tr><tr><td class="src">atomP</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:atomP">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">atTopLevel</td><td class="module"><a href="Agda-Interaction-BasicOps.html#v:atTopLevel">Agda.Interaction.BasicOps</a></td></tr><tr><td class="src">auto</td><td class="module"><a href="Agda-Auto-Auto.html#v:auto">Agda.Auto.Auto</a></td></tr><tr><td class="src">Axiom</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Axiom">Agda.Syntax.Abstract</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete-Definitions.html#v:Axiom">Agda.Syntax.Concrete.Definitions</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:Axiom">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">axiomName</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:axiomName">Agda.Syntax.Abstract</a></td></tr></table></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>