<!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 - E)</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">&</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"><</a></li><li><a href="doc-index-61.html">=</a></li><li><a href="doc-index-62.html">></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 - E</p><table><tr><td class="src">eatNextChar</td><td class="module"><a href="Agda-Syntax-Parser-LookAhead.html#v:eatNextChar">Agda.Syntax.Parser.LookAhead</a></td></tr><tr><td class="src">Edge</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Positivity.html#t:Edge">Agda.TypeChecking.Positivity</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Positivity.html#v:Edge">Agda.TypeChecking.Positivity</a></td></tr><tr><td class="src">edgeIn</td><td class="module"><a href="Agda-Utils-Graph.html#v:edgeIn">Agda.Utils.Graph</a></td></tr><tr><td class="src">edges</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Utils-Graph.html#v:edges">Agda.Utils.Graph</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Utils-Warshall.html#v:edges">Agda.Utils.Warshall</a></td></tr><tr><td class="src">edgesFrom</td><td class="module"><a href="Agda-Utils-Graph.html#v:edgesFrom">Agda.Utils.Graph</a></td></tr><tr><td class="src">EE</td><td class="module"><a href="Agda-Auto-Syntax.html#t:EE">Agda.Auto.Syntax</a></td></tr><tr><td class="src">EInterface</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Compiler-Epic-Interface.html#t:EInterface">Agda.Compiler.Epic.Interface</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Compiler-Epic-Interface.html#v:EInterface">Agda.Compiler.Epic.Interface</a></td></tr><tr><td class="src">EitherOrBoth</td><td class="module"><a href="Agda-Utils-Map.html#t:EitherOrBoth">Agda.Utils.Map</a></td></tr><tr><td class="src">El</td><td class="module"><a href="Agda-Syntax-Internal.html#v:El">Agda.Syntax.Internal</a></td></tr><tr><td class="src">el</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:el">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">elements</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">elementsUnlessEmpty</td><td class="module"><a href="Agda-Utils-TestHelpers.html#v:elementsUnlessEmpty">Agda.Utils.TestHelpers</a></td></tr><tr><td class="src">elems</td><td class="module">Agda.Utils.HashMap</td></tr><tr><td class="src">Elim</td><td class="module"><a href="Agda-Syntax-Internal.html#t:Elim">Agda.Syntax.Internal</a></td></tr><tr><td class="src">ElimCmp</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:ElimCmp">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">ElimView</td><td class="module"><a href="Agda-TypeChecking-Eliminators.html#t:ElimView">Agda.TypeChecking.Eliminators</a></td></tr><tr><td class="src">elimView</td><td class="module"><a href="Agda-TypeChecking-Eliminators.html#v:elimView">Agda.TypeChecking.Eliminators</a></td></tr><tr><td class="src">Ellipsis</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Ellipsis">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">Elr</td><td class="module"><a href="Agda-Auto-Syntax.html#t:Elr">Agda.Auto.Syntax</a></td></tr><tr><td class="src">ElseSh</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:ElseSh">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">emacsifyDebugMessage</td><td class="module"><a href="Agda-TypeChecking-Monad-Options.html#v:emacsifyDebugMessage">Agda.TypeChecking.Monad.Options</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">emap</td><td class="module"><a href="Agda-TypeChecking-Records.html#v:emap">Agda.TypeChecking.Records</a></td></tr><tr><td class="src">EmbPrj</td><td class="module"><a href="Agda-TypeChecking-Serialise.html#t:EmbPrj">Agda.TypeChecking.Serialise</a></td></tr><tr><td class="src">emp</td><td class="module"><a href="Agda-Compiler-JS-Substitution.html#v:emp">Agda.Compiler.JS.Substitution</a></td></tr><tr><td class="src">empty</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Utils-VarSet.html#v:empty">Agda.Utils.VarSet</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="alt">3 (Function)</td><td class="module">Agda.Utils.HashMap</td></tr><tr><td class="alt">4 (Function)</td><td class="module"><a href="Agda-Utils-Trie.html#v:empty">Agda.Utils.Trie</a></td></tr><tr><td class="alt">5 (Function)</td><td class="module"><a href="Agda-Termination-CallGraph.html#v:empty">Agda.Termination.CallGraph</a></td></tr><tr><td class="alt">6 (Function)</td><td class="module"><a href="Agda-Utils-Graph.html#v:empty">Agda.Utils.Graph</a></td></tr><tr><td class="alt">7 (Function)</td><td class="module"><a href="Agda-Interaction-Highlighting-Range.html#v:empty">Agda.Interaction.Highlighting.Range</a></td></tr><tr><td class="alt">8 (Function)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:empty">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="src">emptyBranches</td><td class="module"><a href="Agda-TypeChecking-CompiledClause.html#v:emptyBranches">Agda.TypeChecking.CompiledClause</a></td></tr><tr><td class="src">emptyC</td><td class="module"><a href="Agda-Compiler-Epic-Injection.html#v:emptyC">Agda.Compiler.Epic.Injection</a></td></tr><tr><td class="src">emptyConstraints</td><td class="module"><a href="Agda-Utils-Warshall.html#v:emptyConstraints">Agda.Utils.Warshall</a></td></tr><tr><td class="src">emptyLayout</td><td class="module"><a href="Agda-Syntax-Parser-Layout.html#v:emptyLayout">Agda.Syntax.Parser.Layout</a></td></tr><tr><td class="src">emptyMetaInfo</td><td class="module"><a href="Agda-Syntax-Info.html#v:emptyMetaInfo">Agda.Syntax.Info</a></td></tr><tr><td class="src">emptyNameSpace</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:emptyNameSpace">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">EmptyS</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:EmptyS">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">emptyScope</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:emptyScope">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">emptyScopeInfo</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:emptyScopeInfo">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">emptySignature</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:emptySignature">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">emptySolution</td><td class="module"><a href="Agda-Utils-Warshall.html#v:emptySolution">Agda.Utils.Warshall</a></td></tr><tr><td class="src">EmptyTel</td><td class="module"><a href="Agda-Syntax-Internal.html#v:EmptyTel">Agda.Syntax.Internal</a></td></tr><tr><td class="src">emptyUEnv</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:emptyUEnv">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">emptyUOutput</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:emptyUOutput">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">emptyUState</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:emptyUState">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">empty_layout</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#v:empty_layout">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">enableDisplayForms</td><td class="module"><a href="Agda-TypeChecking-Monad-Options.html#v:enableDisplayForms">Agda.TypeChecking.Monad.Options</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">enablePhantomTypes</td><td class="module"><a href="Agda-TypeChecking-Polarity.html#v:enablePhantomTypes">Agda.TypeChecking.Polarity</a></td></tr><tr><td class="src">encode</td><td class="module"><a href="Agda-TypeChecking-Serialise.html#v:encode">Agda.TypeChecking.Serialise</a></td></tr><tr><td class="src">encodeFile</td><td class="module"><a href="Agda-TypeChecking-Serialise.html#v:encodeFile">Agda.TypeChecking.Serialise</a></td></tr><tr><td class="src">encodeModuleName</td><td class="module"><a href="Agda-Compiler-MAlonzo-Encode.html#v:encodeModuleName">Agda.Compiler.MAlonzo.Encode</a></td></tr><tr><td class="src">end</td><td class="module"><a href="Agda-Syntax-Parser-LexActions.html#v:end">Agda.Syntax.Parser.LexActions</a></td></tr><tr><td class="src">endBy</td><td class="module"><a href="Agda-Utils-ReadP.html#v:endBy">Agda.Utils.ReadP</a></td></tr><tr><td class="src">endBy1</td><td class="module"><a href="Agda-Utils-ReadP.html#v:endBy1">Agda.Utils.ReadP</a></td></tr><tr><td class="src">endWith</td><td class="module"><a href="Agda-Syntax-Parser-LexActions.html#v:endWith">Agda.Syntax.Parser.LexActions</a></td></tr><tr><td class="src">end_</td><td class="module"><a href="Agda-Syntax-Parser-LexActions.html#v:end_">Agda.Syntax.Parser.LexActions</a></td></tr><tr><td class="src">enterClosure</td><td class="module"><a href="Agda-TypeChecking-Monad-Closure.html#v:enterClosure">Agda.TypeChecking.Monad.Closure</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">Env</td><td class="module"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#t:Env">Agda.Syntax.Translation.AbstractToConcrete</a></td></tr><tr><td class="src">envAbstractMode</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envAbstractMode">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envActiveProblems</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envActiveProblems">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envAllowDestructiveUpdate</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envAllowDestructiveUpdate">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envAnonymousModules</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envAnonymousModules">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envAssignMetas</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envAssignMetas">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envCall</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envCall">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envContext</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envContext">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envCurrentModule</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envCurrentModule">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envCurrentPath</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envCurrentPath">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envDisplayFormsEnabled</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envDisplayFormsEnabled">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envEmacs</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envEmacs">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envEtaContractImplicit</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envEtaContractImplicit">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envHighlightingLevel</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envHighlightingLevel">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envHighlightingMethod</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envHighlightingMethod">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envHighlightingRange</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envHighlightingRange">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envImportPath</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envImportPath">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envLetBindings</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envLetBindings">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envModuleNestingLevel</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envModuleNestingLevel">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envMutualBlock</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envMutualBlock">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envRange</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envRange">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envReifyInteractionPoints</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envReifyInteractionPoints">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envRelevance</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envRelevance">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">envSolvingConstraints</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:envSolvingConstraints">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">eof</td><td class="module"><a href="Agda-Syntax-Parser-LexActions.html#v:eof">Agda.Syntax.Parser.LexActions</a></td></tr><tr><td class="src">Epic</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:Epic">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">EpicCode</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:EpicCode">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">epicError</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:epicError">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">EpicFun</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:EpicFun">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">eqelr</td><td class="module"><a href="Agda-Auto-CaseSplit.html#v:eqelr">Agda.Auto.CaseSplit</a></td></tr><tr><td class="src">eqGroups</td><td class="module"><a href="Agda-Compiler-Epic-Injection.html#v:eqGroups">Agda.Compiler.Epic.Injection</a></td></tr><tr><td class="src">eqrcBegin</td><td class="module"><a href="Agda-Auto-Syntax.html#v:eqrcBegin">Agda.Auto.Syntax</a></td></tr><tr><td class="src">eqrcCong</td><td class="module"><a href="Agda-Auto-Syntax.html#v:eqrcCong">Agda.Auto.Syntax</a></td></tr><tr><td class="src">eqrcEnd</td><td class="module"><a href="Agda-Auto-Syntax.html#v:eqrcEnd">Agda.Auto.Syntax</a></td></tr><tr><td class="src">eqrcId</td><td class="module"><a href="Agda-Auto-Syntax.html#v:eqrcId">Agda.Auto.Syntax</a></td></tr><tr><td class="src">eqrcStep</td><td class="module"><a href="Agda-Auto-Syntax.html#v:eqrcStep">Agda.Auto.Syntax</a></td></tr><tr><td class="src">eqrcSym</td><td class="module"><a href="Agda-Auto-Syntax.html#v:eqrcSym">Agda.Auto.Syntax</a></td></tr><tr><td class="src">EqReasoningConsts</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Auto-Syntax.html#t:EqReasoningConsts">Agda.Auto.Syntax</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Auto-Syntax.html#v:EqReasoningConsts">Agda.Auto.Syntax</a></td></tr><tr><td class="src">EqReasoningState</td><td class="module"><a href="Agda-Auto-Syntax.html#t:EqReasoningState">Agda.Auto.Syntax</a></td></tr><tr><td class="src">EqRSChain</td><td class="module"><a href="Agda-Auto-Syntax.html#v:EqRSChain">Agda.Auto.Syntax</a></td></tr><tr><td class="src">EqRSNone</td><td class="module"><a href="Agda-Auto-Syntax.html#v:EqRSNone">Agda.Auto.Syntax</a></td></tr><tr><td class="src">EqRSPrf1</td><td class="module"><a href="Agda-Auto-Syntax.html#v:EqRSPrf1">Agda.Auto.Syntax</a></td></tr><tr><td class="src">EqRSPrf2</td><td class="module"><a href="Agda-Auto-Syntax.html#v:EqRSPrf2">Agda.Auto.Syntax</a></td></tr><tr><td class="src">EqRSPrf3</td><td class="module"><a href="Agda-Auto-Syntax.html#v:EqRSPrf3">Agda.Auto.Syntax</a></td></tr><tr><td class="src">Equal</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:Equal">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">equalAtom</td><td class="module"><a href="Agda-TypeChecking-Conversion.html#v:equalAtom">Agda.TypeChecking.Conversion</a></td></tr><tr><td class="src">Equality</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Equality">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">equalLevel</td><td class="module"><a href="Agda-TypeChecking-Conversion.html#v:equalLevel">Agda.TypeChecking.Conversion</a></td></tr><tr><td class="src">equals</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:equals">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="src">equalSort</td><td class="module"><a href="Agda-TypeChecking-Conversion.html#v:equalSort">Agda.TypeChecking.Conversion</a></td></tr><tr><td class="src">equalTerm</td><td class="module"><a href="Agda-TypeChecking-Conversion.html#v:equalTerm">Agda.TypeChecking.Conversion</a></td></tr><tr><td class="src">equalType</td><td class="module"><a href="Agda-TypeChecking-Conversion.html#v:equalType">Agda.TypeChecking.Conversion</a></td></tr><tr><td class="src">Erasure</td><td class="module"><a href="Agda-Compiler-Epic-Erasure.html#t:Erasure">Agda.Compiler.Epic.Erasure</a></td></tr><tr><td class="src">erasure</td><td class="module"><a href="Agda-Compiler-Epic-Erasure.html#v:erasure">Agda.Compiler.Epic.Erasure</a></td></tr><tr><td class="src">ErasureState</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Compiler-Epic-Erasure.html#t:ErasureState">Agda.Compiler.Epic.Erasure</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Compiler-Epic-Erasure.html#v:ErasureState">Agda.Compiler.Epic.Erasure</a></td></tr><tr><td class="src">eriEqRState</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:eriEqRState">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">eriInfTypeUnknown</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:eriInfTypeUnknown">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">eriIotaStep</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:eriIotaStep">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">eriIsEliminand</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:eriIsEliminand">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">eriMain</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:eriMain">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">eriPickSubsVar</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:eriPickSubsVar">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">eriUnifs</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:eriUnifs">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">eriUsedVars</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:eriUsedVars">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">errInput</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:errInput">Agda.Syntax.Parser.Monad</a>, <a href="Agda-Syntax-Parser.html#v:errInput">Agda.Syntax.Parser</a></td></tr><tr><td class="src">errMsg</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:errMsg">Agda.Syntax.Parser.Monad</a>, <a href="Agda-Syntax-Parser.html#v:errMsg">Agda.Syntax.Parser</a></td></tr><tr><td class="src">Error</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:Error">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Interaction-Highlighting-Precise.html#v:Error">Agda.Interaction.Highlighting.Precise</a></td></tr><tr><td class="src">errPos</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:errPos">Agda.Syntax.Parser.Monad</a>, <a href="Agda-Syntax-Parser.html#v:errPos">Agda.Syntax.Parser</a></td></tr><tr><td class="src">errPrevToken</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:errPrevToken">Agda.Syntax.Parser.Monad</a>, <a href="Agda-Syntax-Parser.html#v:errPrevToken">Agda.Syntax.Parser</a></td></tr><tr><td class="src">escape</td><td class="module"><a href="Agda-Interaction-Highlighting-Vim.html#v:escape">Agda.Interaction.Highlighting.Vim</a></td></tr><tr><td class="src">escapeContext</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:escapeContext">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">escapeContextToTopLevel</td><td class="module"><a href="Agda-TypeChecking-Monad-Context.html#v:escapeContextToTopLevel">Agda.TypeChecking.Monad.Context</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">escChr</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:escChr">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">etaContract</td><td class="module"><a href="Agda-TypeChecking-EtaContract.html#v:etaContract">Agda.TypeChecking.EtaContract</a></td></tr><tr><td class="src">etaContractBody</td><td class="module"><a href="Agda-Auto-Convert.html#v:etaContractBody">Agda.Auto.Convert</a></td></tr><tr><td class="src">etaContractRecord</td><td class="module"><a href="Agda-TypeChecking-Records.html#v:etaContractRecord">Agda.TypeChecking.Records</a></td></tr><tr><td class="src">EtaExpand</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:EtaExpand">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">etaExpand</td><td class="module"><a href="Agda-Compiler-Epic-Static.html#v:etaExpand">Agda.Compiler.Epic.Static</a></td></tr><tr><td class="src">etaExpandBlocked</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:etaExpandBlocked">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">etaExpandClause</td><td class="module"><a href="Agda-TypeChecking-Positivity.html#v:etaExpandClause">Agda.TypeChecking.Positivity</a></td></tr><tr><td class="src">etaExpandListeners</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:etaExpandListeners">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">etaExpandMeta</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:etaExpandMeta">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">etaExpandMetaSafe</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:etaExpandMetaSafe">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">etaExpandRecord</td><td class="module"><a href="Agda-TypeChecking-Records.html#v:etaExpandRecord">Agda.TypeChecking.Records</a></td></tr><tr><td class="src">etaOnce</td><td class="module"><a href="Agda-TypeChecking-EtaContract.html#v:etaOnce">Agda.TypeChecking.EtaContract</a></td></tr><tr><td class="src">EtaPragma</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:EtaPragma">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:EtaPragma">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">ETel</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:ETel">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:ETel">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">evalIn</td><td class="module"><a href="Agda-Interaction-CommandLine-CommandLine.html#v:evalIn">Agda.Interaction.CommandLine.CommandLine</a></td></tr><tr><td class="src">evalInCurrent</td><td class="module"><a href="Agda-Interaction-BasicOps.html#v:evalInCurrent">Agda.Interaction.BasicOps</a></td></tr><tr><td class="src">evalInMeta</td><td class="module"><a href="Agda-Interaction-BasicOps.html#v:evalInMeta">Agda.Interaction.BasicOps</a></td></tr><tr><td class="src">evalTerm</td><td class="module"><a href="Agda-Interaction-CommandLine-CommandLine.html#v:evalTerm">Agda.Interaction.CommandLine.CommandLine</a></td></tr><tr><td class="src">evaluateCC</td><td class="module"><a href="Agda-Compiler-Epic-Static.html#v:evaluateCC">Agda.Compiler.Epic.Static</a></td></tr><tr><td class="src">evaluateTerm</td><td class="module"><a href="Agda-Compiler-Epic-Static.html#v:evaluateTerm">Agda.Compiler.Epic.Static</a></td></tr><tr><td class="src">everythingInScope</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:everythingInScope">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">exact</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:exact">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">Exception</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:Exception">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">ExceptionT</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Monad-Exception.html#t:ExceptionT">Agda.TypeChecking.Monad.Exception</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Monad-Exception.html#v:ExceptionT">Agda.TypeChecking.Monad.Exception</a></td></tr><tr><td class="src">exhaustive</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">ExitCode</td><td class="module"><a href="Agda-Interaction-CommandLine-CommandLine.html#t:ExitCode">Agda.Interaction.CommandLine.CommandLine</a></td></tr><tr><td class="src">Exp</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Auto-Syntax.html#t:Exp">Agda.Auto.Syntax</a></td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#t:Exp">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">exp</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:exp">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">exp0</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:exp0">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">exp1</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:exp1">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">exp2</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:exp2">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">exp2'</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:exp2-39-">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">exp3</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:exp3">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">exp3'</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:exp3-39-">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">expandbind</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:expandbind">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">expandCatchAlls</td><td class="module"><a href="Agda-TypeChecking-CompiledClause-Compile.html#v:expandCatchAlls">Agda.TypeChecking.CompiledClause.Compile</a></td></tr><tr><td class="src">expandExp</td><td class="module"><a href="Agda-Auto-Syntax.html#v:expandExp">Agda.Auto.Syntax</a></td></tr><tr><td class="src">ExpandHidden</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:ExpandHidden">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">ExpandInstanceArguments</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:ExpandInstanceArguments">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">ExpandInstances</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:ExpandInstances">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">ExpandLast</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:ExpandLast">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">expandLitPattern</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Split.html#v:expandLitPattern">Agda.TypeChecking.Rules.LHS.Split</a></td></tr><tr><td class="src">expandP</td><td class="module"><a href="Agda-Utils-Permutation.html#v:expandP">Agda.Utils.Permutation</a></td></tr><tr><td class="src">expectFailure</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">explicitForAll</td><td class="module"><a href="Agda-Compiler-MAlonzo-Compiler.html#v:explicitForAll">Agda.Compiler.MAlonzo.Compiler</a></td></tr><tr><td class="src">expName</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:expName">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">Export</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#t:Export">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:Export">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">exportedNamesInScope</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:exportedNamesInScope">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">exports</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:exports">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Pretty.html#v:exports">Agda.Compiler.JS.Pretty</a></td></tr><tr><td class="src">Expr</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Concrete.html#t:Expr">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#t:Expr">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="alt">3 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:Expr">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">ExpRefInfo</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Auto-SearchControl.html#t:ExpRefInfo">Agda.Auto.SearchControl</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:ExpRefInfo">Agda.Auto.SearchControl</a></td></tr><tr><td class="src">ExprHole</td><td class="module"><a href="Agda-Syntax-Notation.html#v:ExprHole">Agda.Syntax.Notation</a></td></tr><tr><td class="src">ExprInfo</td><td class="module"><a href="Agda-Syntax-Info.html#t:ExprInfo">Agda.Syntax.Info</a></td></tr><tr><td class="src">exprParser</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Parser-Parser.html#v:exprParser">Agda.Syntax.Parser.Parser</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Parser.html#v:exprParser">Agda.Syntax.Parser</a></td></tr><tr><td class="src">ExprRange</td><td class="module"><a href="Agda-Syntax-Info.html#v:ExprRange">Agda.Syntax.Info</a></td></tr><tr><td class="src">ExprSource</td><td class="module"><a href="Agda-Syntax-Info.html#v:ExprSource">Agda.Syntax.Info</a></td></tr><tr><td class="src">ExprView</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#t:ExprView">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">exprView</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:exprView">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">extendConf</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:extendConf">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">ExtendedLam</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:ExtendedLam">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:ExtendedLam">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">ExtendedLambda</td><td class="module"><a href="Agda-Interaction-MakeCase.html#v:ExtendedLambda">Agda.Interaction.MakeCase</a></td></tr><tr><td class="src">extendlambdaname</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:extendlambdaname">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">extendSolution</td><td class="module"><a href="Agda-Utils-Warshall.html#v:extendSolution">Agda.Utils.Warshall</a></td></tr><tr><td class="src">ExtendTel</td><td class="module"><a href="Agda-Syntax-Internal.html#v:ExtendTel">Agda.Syntax.Internal</a></td></tr><tr><td class="src">extendWithTelConf</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:extendWithTelConf">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">extractblkinfos</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:extractblkinfos">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">extractNthElement</td><td class="module"><a href="Agda-Utils-List.html#v:extractNthElement">Agda.Utils.List</a></td></tr><tr><td class="src">extractNthElement'</td><td class="module"><a href="Agda-Utils-List.html#v:extractNthElement-39-">Agda.Utils.List</a></td></tr><tr><td class="src">extraref</td><td class="module"><a href="Agda-Auto-SearchControl.html#v:extraref">Agda.Auto.SearchControl</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>
