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	Agda.Utils.Graph.AdjacencyMap.Unidirectional
LabelledEdge	Agda.TypeChecking.SizedTypes.WarshallSolver
LabelPatVars	Agda.Syntax.Internal.Pattern
labelPatVars	Agda.Syntax.Internal.Pattern
Lam
1 (Data Constructor)	Agda.Syntax.Reflected
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
6 (Data Constructor)	Agda.Auto.Syntax
Lambda
1 (Data Constructor)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Compiler.JS.Syntax
lambda	Agda.Syntax.Concrete.Pretty
LambdaHole	Agda.Syntax.Notation
lambdaLiftExpr	Agda.Syntax.Abstract
LamBinding
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
LamBinding'	Agda.Syntax.Concrete
lamBrackets	Agda.Syntax.Fixity
LamNotPi	Agda.TypeChecking.Rules.Term
LamOrPi	Agda.TypeChecking.Rules.Term
LamV	Agda.Syntax.Concrete.Operators.Parser
LanguagePragma	Agda.Utils.Haskell.Syntax
largest	Agda.TypeChecking.SizedTypes.WarshallSolver
lastMaybe	Agda.Utils.List
LaTeX	Agda.Interaction.InteractionTop
Layer
1 (Type/Class)	Agda.Syntax.Parser.Literate
2 (Data Constructor)	Agda.Syntax.Parser.Literate
layerContent	Agda.Syntax.Parser.Literate
LayerType	Agda.Syntax.Parser.Literate
layerType	Agda.Syntax.Parser.Literate
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.Class, 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
LeaveSection	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
leaveTop	Agda.TypeChecking.MetaVars.Occurs
LeftAssoc	Agda.Syntax.Fixity
LeftDisjunct	Agda.Auto.NarrowingSearch
leftExpr	Agda.TypeChecking.SizedTypes.Syntax
LeftHandSide	Agda.Syntax.Translation.ConcreteToAbstract
LeftMode	Agda.Utils.Pretty
LeftOfArrow	Agda.TypeChecking.Positivity.Occurrence
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
LensArgInfo	Agda.Syntax.Common
LensCommandLineOptions	Agda.Interaction.Options.Lenses
LensConName	Agda.Syntax.Internal
lensField1	Agda.Utils.Lens.Examples
lensField2	Agda.Utils.Lens.Examples
lensFresh	Agda.TypeChecking.Serialise.Base
LensHiding	Agda.Syntax.Common
LensIncludePaths	Agda.Interaction.Options.Lenses
lensLexInput	Agda.Syntax.Parser.Alex
LensOrigin	Agda.Syntax.Common
lensPersistentState	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
LensPersistentVerbosity	Agda.Interaction.Options.Lenses
LensPragmaOptions	Agda.Interaction.Options.Lenses
LensRelevance	Agda.Syntax.Common
lensReuse	Agda.TypeChecking.Serialise.Base
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.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Compiler.Epic.AuxAST
4 (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
LetDeclaredVariable	Agda.Syntax.Abstract
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
lexSrcFile	Agda.Syntax.Parser.Alex
LexState	Agda.Syntax.Parser.Monad
lexToken	Agda.Syntax.Parser.LexActions
lfcCached	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
lfcCurrent	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
lhsAsBindings	Agda.TypeChecking.Rules.LHS
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
lhsParameters	Agda.TypeChecking.Rules.LHS
lhsPats
1 (Function)	Agda.Syntax.Concrete
2 (Function)	Agda.Syntax.Abstract
lhsPatsLeft	Agda.Syntax.Concrete
lhsPatsRight
1 (Function)	Agda.Syntax.Concrete
2 (Function)	Agda.Syntax.Abstract
lhsPatSubst	Agda.TypeChecking.Rules.LHS
lhsPatterns	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
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
libDepends	Agda.Interaction.Library.Base
libFile	Agda.Interaction.Library.Base
libIncludes	Agda.Interaction.Library.Base
LibM	Agda.Interaction.Library
LibName	Agda.Interaction.Library.Base, Agda.Interaction.Library
libName	Agda.Interaction.Library.Base
libraryIncludePaths	Agda.Interaction.Library
libToTCM	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
Lift	Agda.Syntax.Internal, Agda.TypeChecking.Substitute
lift	Agda.Auto.CaseSplit
liftCommandMT	Agda.Interaction.InteractionTop
liftCommandMTLocalState	Agda.Interaction.InteractionTop
liftListT	Agda.Utils.ListT
liftLocalState	Agda.Interaction.InteractionTop
liftP
1 (Function)	Agda.Utils.Permutation
2 (Function)	Agda.Syntax.Parser.LookAhead
liftRed	Agda.TypeChecking.Rewriting.NonLinMatch
liftS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
liftTCM	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
liftU	Agda.TypeChecking.Unquote
liftU1	Agda.TypeChecking.Unquote
liftU2	Agda.TypeChecking.Unquote
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
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.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Syntax.Reflected
3 (Data Constructor)	Agda.Syntax.Concrete
4 (Data Constructor)	Agda.Syntax.Internal
5 (Data Constructor)	Agda.Compiler.Epic.AuxAST
6 (Type/Class)	Agda.Compiler.Epic.AuxAST
7 (Data Constructor)	Agda.Syntax.Abstract
litBranches	Agda.TypeChecking.CompiledClause
litCase	Agda.TypeChecking.CompiledClause
LitChar	Agda.Syntax.Literal
litChar	Agda.Syntax.Parser.StringLiterals
LitDBP	Agda.Termination.Monad
Literal
1 (Type/Class)	Agda.Utils.Haskell.Syntax
2 (Type/Class)	Agda.Syntax.Literal
literal
1 (Function)	Agda.Syntax.Parser.LexActions
2 (Function)	Agda.Compiler.JS.Compiler
3 (Function)	Agda.Compiler.MAlonzo.Compiler
literateExts	Agda.Syntax.Parser.Literate
literateExtsShortList	Agda.Syntax.Parser.Literate
literateProcessors	Agda.Syntax.Parser.Literate
literateRsT	Agda.Syntax.Parser.Literate
literateSrcFile	Agda.Syntax.Parser.Literate
literateTeX	Agda.Syntax.Parser.Literate
LitFloat	Agda.Syntax.Literal
LitFocus	Agda.TypeChecking.Rules.LHS.Problem
litInt	Agda.Compiler.Epic.Injection
LitMeta	Agda.Syntax.Literal
LitNat	Agda.Syntax.Literal
LitP
1 (Data Constructor)	Agda.Syntax.Reflected
2 (Data Constructor)	Agda.Syntax.Concrete
3 (Data Constructor)	Agda.Syntax.Internal
4 (Data Constructor)	Agda.Syntax.Abstract
LitQName	Agda.Syntax.Literal
litqname
1 (Function)	Agda.Compiler.JS.Compiler
2 (Function)	Agda.Compiler.MAlonzo.Compiler
litqnamepat	Agda.Compiler.MAlonzo.Compiler
LitS	Agda.Syntax.Reflected
LitString	Agda.Syntax.Literal
litString
1 (Function)	Agda.Syntax.Parser.StringLiterals
2 (Function)	Agda.Compiler.MAlonzo.Compiler
litToCon	Agda.Compiler.Epic.Injection
litToCore	Agda.Compiler.UHC.FromAgda
litType	Agda.TypeChecking.Monad.Builtin
LoadedFileCache
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
loadFile	Agda.Interaction.CommandLine
Local
1 (Data Constructor)	Agda.Compiler.JS.Syntax
2 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
3 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
local	Agda.Compiler.JS.Compiler
LocalDisplayForm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
LocalId
1 (Type/Class)	Agda.Compiler.JS.Syntax
2 (Data Constructor)	Agda.Compiler.JS.Syntax
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
localStateCommandM	Agda.Interaction.InteractionTop
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.Parser.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.BiMap
3 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
4 (Function)	Agda.Utils.Trie
5 (Function)	Agda.Utils.AssocList
6 (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	Agda.TypeChecking.SizedTypes.WarshallSolver
lookupImportedName	Agda.Syntax.Scope.Monad
lookupIndex	Agda.Compiler.MAlonzo.Compiler
lookupInteractionId	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupInteractionMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupInteractionMeta_	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupInteractionPoint	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupMeta
1 (Function)	Agda.Syntax.Internal.Defs
2 (Function)	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
3 (Function)	Agda.TypeChecking.Reduce.Monad
lookupModuleFromSource	Agda.TypeChecking.Monad.Base, 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.Class, Agda.TypeChecking.Substitute
lookupSection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
lookupTrie	Agda.Utils.Trie
lowerBounds	Agda.TypeChecking.SizedTypes.WarshallSolver
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