<!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 - L)</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 - L</p><table><tr><td class="src">L</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Interaction-EmacsCommand.html#v:L">Agda.Interaction.EmacsCommand</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Utils-Map.html#v:L">Agda.Utils.Map</a></td></tr><tr><td class="src">label</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">labels</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">Lam</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Auto-Syntax.html#v:Lam">Agda.Auto.Syntax</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Lam">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Lam">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">4 (Data Constructor)</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:Lam">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="alt">5 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Lam">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">Lambda</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:Lambda">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">lambda</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Case.html#v:lambda">Agda.Compiler.JS.Case</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Concrete-Pretty.html#v:lambda">Agda.Syntax.Concrete.Pretty</a></td></tr><tr><td class="src">lambda'</td><td class="module"><a href="Agda-Compiler-JS-Case.html#v:lambda-39-">Agda.Compiler.JS.Case</a></td></tr><tr><td class="src">LambdaHole</td><td class="module"><a href="Agda-Syntax-Notation.html#v:LambdaHole">Agda.Syntax.Notation</a></td></tr><tr><td class="src">lambdaLiftExpr</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lambdaLiftExpr">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LamBinding</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Concrete.html#t:LamBinding">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:LamBinding">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lamBrackets</td><td class="module"><a href="Agda-Syntax-Fixity.html#v:lamBrackets">Agda.Syntax.Fixity</a></td></tr><tr><td class="src">lamFreq</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:lamFreq">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">LamNotPi</td><td class="module"><a href="Agda-TypeChecking-Rules-Term.html#v:LamNotPi">Agda.TypeChecking.Rules.Term</a></td></tr><tr><td class="src">LamOrPi</td><td class="module"><a href="Agda-TypeChecking-Rules-Term.html#t:LamOrPi">Agda.TypeChecking.Rules.Term</a></td></tr><tr><td class="src">LamV</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:LamV">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">Layout</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:Layout">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">layout</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#v:layout">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">LayoutContext</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#t:LayoutContext">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">layoutKeywords</td><td class="module"><a href="Agda-Syntax-Parser-Tokens.html#v:layoutKeywords">Agda.Syntax.Parser.Tokens</a></td></tr><tr><td class="src">Lazy</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:Lazy">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">lazy</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:lazy">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">lblBindings</td><td class="module"><a href="Agda-TypeChecking-Coverage-SplitTree.html#v:lblBindings">Agda.TypeChecking.Coverage.SplitTree</a></td></tr><tr><td class="src">lblConstructorName</td><td class="module"><a href="Agda-TypeChecking-Coverage-SplitTree.html#v:lblConstructorName">Agda.TypeChecking.Coverage.SplitTree</a></td></tr><tr><td class="src">lblSplitArg</td><td class="module"><a href="Agda-TypeChecking-Coverage-SplitTree.html#v:lblSplitArg">Agda.TypeChecking.Coverage.SplitTree</a></td></tr><tr><td class="src">lbrace</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="src">lbrack</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="src">LChar</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:LChar">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">le</td><td class="module"><a href="Agda-Termination-CallGraph.html#v:le">Agda.Termination.CallGraph</a></td></tr><tr><td class="src">leaveTop</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#v:leaveTop">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">LeftAssoc</td><td class="module"><a href="Agda-Syntax-Fixity.html#v:LeftAssoc">Agda.Syntax.Fixity</a></td></tr><tr><td class="src">LeftDisjunct</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:LeftDisjunct">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">leftDistributive</td><td class="module"><a href="Agda-Utils-TestHelpers.html#v:leftDistributive">Agda.Utils.TestHelpers</a></td></tr><tr><td class="src">LeftHandSide</td><td class="module"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:LeftHandSide">Agda.Syntax.Translation.ConcreteToAbstract</a></td></tr><tr><td class="src">leftHH</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:leftHH">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">LeftMode</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="src">LeftOfArrow</td><td class="module"><a href="Agda-TypeChecking-Positivity.html#v:LeftOfArrow">Agda.TypeChecking.Positivity</a></td></tr><tr><td class="src">LeftOperandCtx</td><td class="module"><a href="Agda-Syntax-Fixity.html#v:LeftOperandCtx">Agda.Syntax.Fixity</a></td></tr><tr><td class="src">LegendMatrix</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Utils-Warshall.html#t:LegendMatrix">Agda.Utils.Warshall</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Utils-Warshall.html#v:LegendMatrix">Agda.Utils.Warshall</a></td></tr><tr><td class="src">Leq</td><td class="module"><a href="Agda-TypeChecking-SizedTypes.html#v:Leq">Agda.TypeChecking.SizedTypes</a></td></tr><tr><td class="src">leqLevel</td><td class="module"><a href="Agda-TypeChecking-Conversion.html#v:leqLevel">Agda.TypeChecking.Conversion</a></td></tr><tr><td class="src">leqSort</td><td class="module"><a href="Agda-TypeChecking-Conversion.html#v:leqSort">Agda.TypeChecking.Conversion</a></td></tr><tr><td class="src">leqType</td><td class="module"><a href="Agda-TypeChecking-Conversion.html#v:leqType">Agda.TypeChecking.Conversion</a></td></tr><tr><td class="src">leqType_</td><td class="module"><a href="Agda-TypeChecking-Rules-Term.html#v:leqType_">Agda.TypeChecking.Rules.Term</a></td></tr><tr><td class="src">Let</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Let">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:Let">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Let">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LetApply</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:LetApply">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LetBind</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:LetBind">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LetBinding</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:LetBinding">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LetBindings</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:LetBindings">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">LetDef</td><td class="module"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:LetDef">Agda.Syntax.Translation.ConcreteToAbstract</a></td></tr><tr><td class="src">LetDefs</td><td class="module"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#t:LetDefs">Agda.Syntax.Translation.ConcreteToAbstract</a></td></tr><tr><td class="src">LetInfo</td><td class="module"><a href="Agda-Syntax-Info.html#t:LetInfo">Agda.Syntax.Info</a></td></tr><tr><td class="src">LetOpen</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:LetOpen">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LetPatBind</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:LetPatBind">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LetRange</td><td class="module"><a href="Agda-Syntax-Info.html#v:LetRange">Agda.Syntax.Info</a></td></tr><tr><td class="src">lett</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:lett">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">Level</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Internal.html#t:Level">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Level">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">3 (Type/Class)</td><td class="module"><a href="Agda-Interaction-Highlighting-Generate.html#t:Level">Agda.Interaction.Highlighting.Generate</a></td></tr><tr><td class="src">LevelAtom</td><td class="module"><a href="Agda-Syntax-Internal.html#t:LevelAtom">Agda.Syntax.Internal</a></td></tr><tr><td class="src">LevelCmp</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:LevelCmp">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">LevelKit</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Level.html#t:LevelKit">Agda.TypeChecking.Level</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Level.html#v:LevelKit">Agda.TypeChecking.Level</a></td></tr><tr><td class="src">levelLub</td><td class="module"><a href="Agda-TypeChecking-Level.html#v:levelLub">Agda.TypeChecking.Level</a></td></tr><tr><td class="src">levelMax</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:levelMax">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">Levels</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:Levels">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">levelSort</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:levelSort">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">levelSuc</td><td class="module"><a href="Agda-Syntax-Internal.html#v:levelSuc">Agda.Syntax.Internal</a></td></tr><tr><td class="src">levelSucFunction</td><td class="module"><a href="Agda-TypeChecking-Level.html#v:levelSucFunction">Agda.TypeChecking.Level</a></td></tr><tr><td class="src">levelTm</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:levelTm">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">levelView</td><td class="module"><a href="Agda-TypeChecking-Level.html#v:levelView">Agda.TypeChecking.Level</a></td></tr><tr><td class="src">LexAction</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#t:LexAction">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="src">lexer</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#v:lexer">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">lexError</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#v:lexError">Agda.Syntax.Parser.Monad</a>, <a href="Agda-Syntax-Parser-LexActions.html#v:lexError">Agda.Syntax.Parser.LexActions</a></td></tr><tr><td class="src">lexInput</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#v:lexInput">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="src">LexOrder</td><td class="module"><a href="Agda-Termination-Lexicographic.html#t:LexOrder">Agda.Termination.Lexicographic</a></td></tr><tr><td class="src">lexOrder</td><td class="module"><a href="Agda-Termination-Lexicographic.html#v:lexOrder">Agda.Termination.Lexicographic</a></td></tr><tr><td class="src">lexPos</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#v:lexPos">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="src">LexPredicate</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#t:LexPredicate">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="src">lexPrevChar</td><td class="module"><a href="Agda-Syntax-Parser-Alex.html#v:lexPrevChar">Agda.Syntax.Parser.Alex</a></td></tr><tr><td class="src">LexState</td><td class="module"><a href="Agda-Syntax-Parser-Monad.html#t:LexState">Agda.Syntax.Parser.Monad</a></td></tr><tr><td class="src">lexToken</td><td class="module"><a href="Agda-Syntax-Parser-LexActions.html#v:lexToken">Agda.Syntax.Parser.LexActions</a></td></tr><tr><td class="src">LFloat</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:LFloat">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">LHS</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Concrete.html#t:LHS">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:LHS">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">3 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:LHS">Agda.Syntax.Abstract</a></td></tr><tr><td class="alt">4 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:LHS">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsAsB</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:lhsAsB">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">LHSCore</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Concrete.html#t:LHSCore">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:LHSCore">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsCore</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsCore">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LHSCore'</td><td class="module"><a href="Agda-Syntax-Abstract.html#t:LHSCore-39-">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsCoreAllPatterns</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsCoreAllPatterns">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsCoreToPattern</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsCoreToPattern">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsCoreToSpine</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsCoreToSpine">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsDefName</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:lhsDefName">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsDefName">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsDestructor</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:lhsDestructor">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsDestructor">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsDPI</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:lhsDPI">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">lhsFocus</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:lhsFocus">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsFocus">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LHSHead</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:LHSHead">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:LHSHead">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LHSInfo</td><td class="module"><a href="Agda-Syntax-Info.html#t:LHSInfo">Agda.Syntax.Info</a></td></tr><tr><td class="src">lhsInfo</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsInfo">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsOriginalPattern</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:lhsOriginalPattern">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">LHSOrPatSyn</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:LHSOrPatSyn">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">lhsPats</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:lhsPats">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsPats">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsPatsLeft</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:lhsPatsLeft">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsPatsLeft">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsPatsRight</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:lhsPatsRight">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsPatsRight">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsProblem</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:lhsProblem">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">LHSProj</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:LHSProj">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:LHSProj">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LHSRange</td><td class="module"><a href="Agda-Syntax-Info.html#v:LHSRange">Agda.Syntax.Info</a></td></tr><tr><td class="src">lhsRewriteEqn</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:lhsRewriteEqn">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">LHSState</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#t:LHSState">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:LHSState">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">lhsSubst</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:lhsSubst">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">lhsToSpine</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsToSpine">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsWithExpr</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:lhsWithExpr">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">lhsWithPats</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:lhsWithPats">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">lhsWithPattern</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:lhsWithPattern">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">Lift</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:Lift">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">lift</td><td class="module"><a href="Agda-Auto-CaseSplit.html#v:lift">Agda.Auto.CaseSplit</a></td></tr><tr><td class="src">liftCommandM</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:liftCommandM">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">liftCommandMT</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:liftCommandMT">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">liftP</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Utils-Permutation.html#v:liftP">Agda.Utils.Permutation</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Parser-LookAhead.html#v:liftP">Agda.Syntax.Parser.LookAhead</a></td></tr><tr><td class="src">liftS</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:liftS">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">liftTCM</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:liftTCM">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">liftUnderAbs</td><td class="module"><a href="Agda-TypeChecking-MetaVars-Occurs.html#v:liftUnderAbs">Agda.TypeChecking.MetaVars.Occurs</a></td></tr><tr><td class="src">lineLength</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="src">LInt</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:LInt">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">Lisp</td><td class="module"><a href="Agda-Interaction-EmacsCommand.html#t:Lisp">Agda.Interaction.EmacsCommand</a></td></tr><tr><td class="src">lispifyHighlightingInfo</td><td class="module"><a href="Agda-Interaction-Highlighting-Emacs.html#v:lispifyHighlightingInfo">Agda.Interaction.Highlighting.Emacs</a></td></tr><tr><td class="src">list</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:list">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">List2</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Utils-Tuple.html#t:List2">Agda.Utils.Tuple</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Utils-Tuple.html#v:List2">Agda.Utils.Tuple</a></td></tr><tr><td class="src">list2</td><td class="module"><a href="Agda-Utils-Tuple.html#v:list2">Agda.Utils.Tuple</a></td></tr><tr><td class="src">Listener</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:Listener">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">listenToMeta</td><td class="module"><a href="Agda-TypeChecking-Monad-MetaVars.html#v:listenToMeta">Agda.TypeChecking.Monad.MetaVars</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">listOf</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">listOf1</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">listOfElements</td><td class="module"><a href="Agda-Utils-TestHelpers.html#v:listOfElements">Agda.Utils.TestHelpers</a></td></tr><tr><td class="src">listToMaybe</td><td class="module">Agda.Utils.Maybe</td></tr><tr><td class="src">Lit</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:Lit">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Lit">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:Lit">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="alt">4 (Type/Class)</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#t:Lit">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="alt">5 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:Lit">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">litBranches</td><td class="module"><a href="Agda-TypeChecking-CompiledClause.html#v:litBranches">Agda.TypeChecking.CompiledClause</a></td></tr><tr><td class="src">litCase</td><td class="module"><a href="Agda-TypeChecking-CompiledClause.html#v:litCase">Agda.TypeChecking.CompiledClause</a></td></tr><tr><td class="src">LitChar</td><td class="module"><a href="Agda-Syntax-Literal.html#v:LitChar">Agda.Syntax.Literal</a></td></tr><tr><td class="src">litChar</td><td class="module"><a href="Agda-Syntax-Parser-StringLiterals.html#v:litChar">Agda.Syntax.Parser.StringLiterals</a></td></tr><tr><td class="src">litCon</td><td class="module"><a href="Agda-Compiler-Epic-Injection.html#v:litCon">Agda.Compiler.Epic.Injection</a></td></tr><tr><td class="src">Literal</td><td class="module"><a href="Agda-Syntax-Literal.html#t:Literal">Agda.Syntax.Literal</a></td></tr><tr><td class="src">literal</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Syntax-Parser-LexActions.html#v:literal">Agda.Syntax.Parser.LexActions</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Compiler-MAlonzo-Compiler.html#v:literal">Agda.Compiler.MAlonzo.Compiler</a></td></tr><tr><td class="alt">3 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Compiler.html#v:literal">Agda.Compiler.JS.Compiler</a></td></tr><tr><td class="src">literate</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#v:literate">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">LitFloat</td><td class="module"><a href="Agda-Syntax-Literal.html#v:LitFloat">Agda.Syntax.Literal</a></td></tr><tr><td class="src">LitFocus</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Problem.html#v:LitFocus">Agda.TypeChecking.Rules.LHS.Problem</a></td></tr><tr><td class="src">litFreq</td><td class="module"><a href="Agda-TypeChecking-Test-Generators.html#v:litFreq">Agda.TypeChecking.Test.Generators</a></td></tr><tr><td class="src">LitInt</td><td class="module"><a href="Agda-Syntax-Literal.html#v:LitInt">Agda.Syntax.Literal</a></td></tr><tr><td class="src">LitMP</td><td class="module"><a href="Agda-TypeChecking-Coverage-Match.html#v:LitMP">Agda.TypeChecking.Coverage.Match</a></td></tr><tr><td class="src">LitP</td><td> </td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:LitP">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Internal.html#v:LitP">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:LitP">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">LitQName</td><td class="module"><a href="Agda-Syntax-Literal.html#v:LitQName">Agda.Syntax.Literal</a></td></tr><tr><td class="src">litqname</td><td class="module"><a href="Agda-Compiler-MAlonzo-Compiler.html#v:litqname">Agda.Compiler.MAlonzo.Compiler</a></td></tr><tr><td class="src">LitSh</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:LitSh">Agda.TypeChecking.Rules.LHS.Unify</a></td></tr><tr><td class="src">LitString</td><td class="module"><a href="Agda-Syntax-Literal.html#v:LitString">Agda.Syntax.Literal</a></td></tr><tr><td class="src">litString</td><td class="module"><a href="Agda-Syntax-Parser-StringLiterals.html#v:litString">Agda.Syntax.Parser.StringLiterals</a></td></tr><tr><td class="src">litToCon</td><td class="module"><a href="Agda-Compiler-Epic-Injection.html#v:litToCon">Agda.Compiler.Epic.Injection</a></td></tr><tr><td class="src">litType</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:litType">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">loadFile</td><td class="module"><a href="Agda-Interaction-CommandLine-CommandLine.html#v:loadFile">Agda.Interaction.CommandLine.CommandLine</a></td></tr><tr><td class="src">Local</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:Local">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">LocalId</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#t:LocalId">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:LocalId">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">localid</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:localid">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">localNameSpace</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:localNameSpace">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">localScope</td><td class="module"><a href="Agda-TypeChecking-Monad-State.html#v:localScope">Agda.TypeChecking.Monad.State</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">localState</td><td class="module"><a href="Agda-Utils-Monad.html#v:localState">Agda.Utils.Monad</a></td></tr><tr><td class="src">localTerminationEnv</td><td class="module"><a href="Agda-Auto-CaseSplit.html#v:localTerminationEnv">Agda.Auto.CaseSplit</a></td></tr><tr><td class="src">localTerminationSidecond</td><td class="module"><a href="Agda-Auto-CaseSplit.html#v:localTerminationSidecond">Agda.Auto.CaseSplit</a></td></tr><tr><td class="src">localToAbstract</td><td class="module"><a href="Agda-Syntax-Translation-ConcreteToAbstract.html#v:localToAbstract">Agda.Syntax.Translation.ConcreteToAbstract</a></td></tr><tr><td class="src">LocalV</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:LocalV">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">LocalVars</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#t:LocalVars">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">LocalVsImportedModuleClash</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:LocalVsImportedModuleClash">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">look</td><td class="module"><a href="Agda-Utils-ReadP.html#v:look">Agda.Utils.ReadP</a></td></tr><tr><td class="src">LookAhead</td><td class="module"><a href="Agda-Syntax-Parser-LookAhead.html#t:LookAhead">Agda.Syntax.Parser.LookAhead</a></td></tr><tr><td class="src">lookInterface</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:lookInterface">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">Lookup</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:Lookup">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">lookup</td><td> </td></tr><tr><td class="alt">1 (Function)</td><td class="module">Agda.Utils.HashMap</td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Utils-Graph.html#v:lookup">Agda.Utils.Graph</a></td></tr><tr><td class="alt">3 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Substitution.html#v:lookup">Agda.Compiler.JS.Substitution</a></td></tr><tr><td class="src">lookupDefault</td><td class="module">Agda.Utils.HashMap</td></tr><tr><td class="src">lookupEdge</td><td class="module"><a href="Agda-Utils-Warshall.html#v:lookupEdge">Agda.Utils.Warshall</a></td></tr><tr><td class="src">lookupInteractionId</td><td class="module"><a href="Agda-TypeChecking-Monad-MetaVars.html#v:lookupInteractionId">Agda.TypeChecking.Monad.MetaVars</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">lookupMeta</td><td class="module"><a href="Agda-TypeChecking-Monad-MetaVars.html#v:lookupMeta">Agda.TypeChecking.Monad.MetaVars</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">lookupMutualBlock</td><td class="module"><a href="Agda-TypeChecking-Monad-Mutual.html#v:lookupMutualBlock">Agda.TypeChecking.Monad.Mutual</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">lookupPath</td><td class="module"><a href="Agda-Utils-Trie.html#v:lookupPath">Agda.Utils.Trie</a></td></tr><tr><td class="src">lookupPatternSyn</td><td class="module"><a href="Agda-TypeChecking-Monad-State.html#v:lookupPatternSyn">Agda.TypeChecking.Monad.State</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">lookupPrimitiveFunction</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:lookupPrimitiveFunction">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">lookupPrimitiveFunctionQ</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:lookupPrimitiveFunctionQ">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">lookupS</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:lookupS">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">lookupSection</td><td class="module"><a href="Agda-TypeChecking-Monad-Signature.html#v:lookupSection">Agda.TypeChecking.Monad.Signature</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">LowerMeta</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#t:LowerMeta">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">lowerMeta</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#v:lowerMeta">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">lowMetaPriority</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:lowMetaPriority">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">lparen</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="src">LString</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:LString">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">lt</td><td class="module"><a href="Agda-Termination-CallGraph.html#v:lt">Agda.Termination.CallGraph</a></td></tr><tr><td class="src">Lvl</td><td> </td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#t:Lvl">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:Lvl">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">lvlMax</td><td class="module"><a href="Agda-TypeChecking-Level.html#v:lvlMax">Agda.TypeChecking.Level</a></td></tr><tr><td class="src">lvlSuc</td><td class="module"><a href="Agda-TypeChecking-Level.html#v:lvlSuc">Agda.TypeChecking.Level</a></td></tr><tr><td class="src">lvlType</td><td class="module"><a href="Agda-TypeChecking-Level.html#v:lvlType">Agda.TypeChecking.Level</a></td></tr><tr><td class="src">lvlView</td><td class="module"><a href="Agda-TypeChecking-Substitute.html#v:lvlView">Agda.TypeChecking.Substitute</a></td></tr><tr><td class="src">lvlZero</td><td class="module"><a href="Agda-TypeChecking-Level.html#v:lvlZero">Agda.TypeChecking.Level</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>
