A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
$
&
+
.
/
<
=
>
|
-
All

Index - L

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