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.Utils.Map
2 (Data Constructor)	Agda.Interaction.EmacsCommand
Label
1 (Type/Class)	Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Data Constructor)	Agda.TypeChecking.SizedTypes.WarshallSolver
label
1 (Function)	Agda.Utils.QuickCheck
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
LabelledEdge	Agda.TypeChecking.SizedTypes.WarshallSolver
LabelPatVars	Agda.Syntax.Internal.Pattern
labelPatVars	Agda.Syntax.Internal.Pattern
labels	Agda.Utils.QuickCheck
Lam
1 (Data Constructor)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Syntax.Abstract
4 (Data Constructor)	Agda.Syntax.Internal
5 (Data Constructor)	Agda.Compiler.Epic.AuxAST
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
lambdas	Agda.Compiler.MAlonzo.Compiler
lambdasUpTo	Agda.Compiler.MAlonzo.Compiler
LamBinding
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
LamBinding'	Agda.Syntax.Concrete
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
Large
1 (Data Constructor)	Agda.Utils.QuickCheck
2 (Type/Class)	Agda.Utils.QuickCheck
largest	Agda.TypeChecking.SizedTypes.WarshallSolver
lastMaybe	Agda.Utils.List
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
lazyAbsApp	Agda.TypeChecking.Substitute
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
lcmp	Agda.TypeChecking.SizedTypes.WarshallSolver
Le	Agda.TypeChecking.SizedTypes.Syntax
le	Agda.Termination.Order
Least	Agda.TypeChecking.SizedTypes.Syntax
leaveTop	Agda.TypeChecking.MetaVars.Occurs
LeftAssoc	Agda.Syntax.Fixity
LeftDisjunct	Agda.Auto.NarrowingSearch
leftDistributive	Agda.Utils.TestHelpers
leftExpr	Agda.TypeChecking.SizedTypes.Syntax
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
Lens'	Agda.Utils.Lens
lensAccumStatistics	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
lensAccumStatisticsP	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
lensAmodName	Agda.Syntax.Scope.Base
lensAnameName	Agda.Syntax.Scope.Base
LensCommandLineOptions	Agda.Interaction.Options.Lenses
LensConName	Agda.Syntax.Internal
lensField1	Agda.Utils.Lens.Examples
lensField2	Agda.Utils.Lens.Examples
LensHiding	Agda.Syntax.Common
LensIncludeDirs	Agda.Interaction.Options.Lenses
lensLexInput	Agda.Syntax.Parser.Alex
lensPersistentState	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
LensPersistentVerbosity	Agda.Interaction.Options.Lenses
LensPragmaOptions	Agda.Interaction.Options.Lenses
LensRelevance	Agda.Syntax.Common
LensSafeMode	Agda.Interaction.Options.Lenses
LensSort	Agda.Syntax.Internal
lensSort	Agda.Syntax.Internal
LensVerbosity	Agda.Interaction.Options.Lenses
Leq	Agda.TypeChecking.SizedTypes
leqLevel	Agda.TypeChecking.Conversion
leqPO	Agda.Utils.PartialOrd
leqSort	Agda.TypeChecking.Conversion
leqType	Agda.TypeChecking.Conversion
leqType_	Agda.TypeChecking.Rules.Term
Let
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
3 (Data Constructor)	Agda.Compiler.Epic.AuxAST
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 (Data Constructor)	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
2 (Type/Class)	Agda.Syntax.Internal
3 (Data Constructor)	Agda.Syntax.Internal
4 (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
LevelReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Levels	Agda.TypeChecking.MetaVars
levelSort	Agda.TypeChecking.Substitute
levelSuc	Agda.Syntax.Internal
levelSucFunction	Agda.TypeChecking.Level
levelTm	Agda.TypeChecking.Substitute
levelType	Agda.TypeChecking.Level
levelView	Agda.TypeChecking.Level
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
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
lhsBodyType	Agda.TypeChecking.Rules.LHS
LHSCore
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
lhsCore	Agda.Syntax.Abstract
LHSCore'	Agda.Syntax.Abstract
lhsCoreAddSpine	Agda.Syntax.Abstract
lhsCoreAllPatterns	Agda.Syntax.Abstract
lhsCoreApp	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
lhsPatterns	Agda.TypeChecking.Rules.LHS
lhsPermutation	Agda.TypeChecking.Rules.LHS
lhsProblem	Agda.TypeChecking.Rules.LHS.Problem
LHSProj
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
LHSRange	Agda.Syntax.Info
LHSResult
1 (Type/Class)	Agda.TypeChecking.Rules.LHS
2 (Data Constructor)	Agda.TypeChecking.Rules.LHS
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
lhsToSpine	Agda.Syntax.Abstract
lhsVarTele	Agda.TypeChecking.Rules.LHS
lhsWithExpr	Agda.Syntax.Concrete
lhsWithPats	Agda.Syntax.Abstract
lhsWithPattern	Agda.Syntax.Concrete
Lift	Agda.Syntax.Internal, Agda.TypeChecking.Substitute
lift	Agda.Auto.CaseSplit
liftCommandMT	Agda.Interaction.InteractionTop
liftP
1 (Function)	Agda.Syntax.Parser.LookAhead
2 (Function)	Agda.Utils.Permutation
liftRed	Agda.TypeChecking.Rewriting.NonLinMatch
liftS	Agda.TypeChecking.Substitute
liftTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
liftUnderAbs	Agda.TypeChecking.MetaVars.Occurs
lineLength	Agda.Utils.Pretty
LInf	Agda.TypeChecking.SizedTypes.WarshallSolver
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
listCase	Agda.Utils.List
listenDirty	Agda.Utils.Update
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
ListT
1 (Type/Class)	Agda.Utils.ListT
2 (Data Constructor)	Agda.Utils.ListT
ListTel	Agda.TypeChecking.Substitute
ListTel'	Agda.TypeChecking.Substitute
listToMaybe
1 (Function)	Agda.Utils.Maybe
2 (Function)	Agda.Utils.Maybe.Strict
Lit
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
3 (Data Constructor)	Agda.Syntax.Internal
4 (Data Constructor)	Agda.Compiler.Epic.AuxAST
5 (Type/Class)	Agda.Compiler.Epic.AuxAST
litAlts	Agda.Compiler.MAlonzo.Compiler
litBranches	Agda.TypeChecking.CompiledClause
litCase	Agda.TypeChecking.CompiledClause
LitChar	Agda.Syntax.Literal
litChar	Agda.Syntax.Parser.StringLiterals
LitDBP	Agda.Termination.Monad
Literal	Agda.Syntax.Literal
literal
1 (Function)	Agda.Syntax.Parser.LexActions
2 (Function)	Agda.Compiler.JS.Compiler
3 (Function)	Agda.Compiler.MAlonzo.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
litInt	Agda.Compiler.Epic.Injection
LitMP	Agda.TypeChecking.Coverage.Match
LitP
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
3 (Data Constructor)	Agda.Syntax.Internal
LitQName	Agda.Syntax.Literal
litqname	Agda.Compiler.MAlonzo.Compiler
litqnamepat	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
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
locally	Agda.Utils.Lens
localNameSpace	Agda.Syntax.Scope.Base
localScope	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
localShadowedBy	Agda.Syntax.Scope.Base
localState	Agda.Utils.Monad
localTCState	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
localTCStateSaving	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
localTerminationEnv	Agda.Auto.CaseSplit
localTerminationSidecond	Agda.Auto.CaseSplit
localToAbstract	Agda.Syntax.Translation.ConcreteToAbstract
LocalV	Agda.Syntax.Concrete.Operators.Parser
LocalVar
1 (Type/Class)	Agda.Syntax.Scope.Base
2 (Data Constructor)	Agda.Syntax.Scope.Base
localVar	Agda.Syntax.Scope.Base
LocalVars	Agda.Syntax.Scope.Base
LocalVsImportedModuleClash	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
loffset	Agda.TypeChecking.SizedTypes.WarshallSolver
LoneProjectionLike	Agda.TypeChecking.ProjectionLike
look	Agda.Utils.ReadP
LookAhead	Agda.Syntax.Parser.LookAhead
lookInterface	Agda.Compiler.Epic.CompileState
Lookup	Agda.Compiler.JS.Syntax
lookup
1 (Function)	Agda.Utils.BiMap
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.AssocList
4 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
5 (Function)	Agda.Compiler.JS.Substitution
lookupBV	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
lookupDefault	Agda.Utils.HashMap
lookupDefinition	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
lookupEdge
1 (Function)	Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Function)	Agda.Utils.Warshall
lookupIndex	Agda.Compiler.MAlonzo.Compiler
lookupInteractionId	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupInteractionPoint	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupLevel	Agda.Compiler.MAlonzo.Compiler
lookupMeta
1 (Function)	Agda.Syntax.Internal.Defs
2 (Function)	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
3 (Function)	Agda.TypeChecking.Reduce.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
lowerBounds	Agda.TypeChecking.SizedTypes.WarshallSolver
lowerMeta	Agda.Interaction.InteractionTop
lowMetaPriority	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
lparen	Agda.Utils.Pretty
LString	Agda.Compiler.Epic.AuxAST
Lt	Agda.TypeChecking.SizedTypes.Syntax
lt	Agda.Termination.Order
ltrim	Agda.Utils.String
lub	Agda.TypeChecking.SizedTypes.WarshallSolver
lub'	Agda.TypeChecking.SizedTypes.WarshallSolver
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