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.Auto.Options
2 (Data Constructor)	Agda.Utils.Map
3 (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.Auto.Syntax
2 (Data Constructor)	Agda.Syntax.Reflected
3 (Data Constructor)	Agda.Syntax.Concrete
4 (Data Constructor)	Agda.Syntax.Internal
5 (Data Constructor)	Agda.Syntax.Abstract
Lambda
1 (Data Constructor)	Agda.Utils.Haskell.Syntax
2 (Data Constructor)	Agda.Compiler.JS.Syntax
lambda	Agda.Syntax.Concrete.Pretty
lambdaAddContext	Agda.TypeChecking.Rules.Term
LambdaHole	Agda.Syntax.Notation
lambdaIrrelevanceCheck	Agda.TypeChecking.Rules.Term
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
lamBrackets'	Agda.Syntax.Fixity
LamInfo
1 (Type/Class)	Agda.Syntax.Info
2 (Data Constructor)	Agda.Syntax.Info
LamNotPi	Agda.TypeChecking.Rules.Term
lamOrigin	Agda.Syntax.Info
LamOrPi	Agda.TypeChecking.Rules.Term
lamParens	Agda.Syntax.Info
lamRange	Agda.Syntax.Info
LamV	Agda.Syntax.Concrete.Operators.Parser
LamView
1 (Type/Class)	Agda.Syntax.Abstract.Views
2 (Data Constructor)	Agda.Syntax.Abstract.Views
lamView	Agda.Syntax.Abstract.Views
LanguagePragma	Agda.Utils.Haskell.Syntax
largest	Agda.TypeChecking.SizedTypes.WarshallSolver
last2	Agda.Utils.List
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
LayerRole	Agda.Syntax.Parser.Literate
layerRole	Agda.Syntax.Parser.Literate
Layers	Agda.Syntax.Parser.Literate
Layout	Agda.Syntax.Parser.Monad
layout	Agda.Syntax.Parser.Lexer
LayoutContext	Agda.Syntax.Parser.Monad
layoutKeywords	Agda.Syntax.Parser.Tokens
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
lcmp	Agda.TypeChecking.SizedTypes.WarshallSolver
Le	Agda.TypeChecking.SizedTypes.Syntax
le	Agda.Termination.Order
Least	Agda.TypeChecking.SizedTypes.Syntax
LeaveAlone	Agda.Interaction.Options
LeaveSection	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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, Agda.Compiler.Backend
lensAccumStatisticsP	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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, Agda.Compiler.Backend
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.Syntax.Abstract
LetApply	Agda.Syntax.Abstract
LetBind	Agda.Syntax.Abstract
LetBinding	Agda.Syntax.Abstract
LetBindings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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, Agda.Compiler.Backend
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, Agda.Compiler.Backend
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, Agda.Compiler.Backend
lfcCurrent	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lFst	Agda.Utils.Lens
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, Agda.Compiler.Backend
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
lhsShouldBeEmptyTypes	Agda.TypeChecking.Rules.LHS.Problem
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
libNameForCurrentDir	Agda.Interaction.Library.Base
libraryIncludePaths	Agda.Interaction.Library
libToTCM	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Lift
1 (Type/Class)	Agda.Auto.CaseSplit
2 (Data Constructor)	Agda.Syntax.Internal, Agda.TypeChecking.Substitute
lift	Agda.Auto.CaseSplit
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, Agda.Compiler.Backend
liftU	Agda.TypeChecking.Unquote
liftU1	Agda.TypeChecking.Unquote
liftU2	Agda.TypeChecking.Unquote
liftUnderAbs	Agda.TypeChecking.MetaVars.Occurs
lIndex	Agda.Utils.IndexedList
lineLength	Agda.Utils.Pretty
LineNumber	Agda.Interaction.Library.Parse
LInf	Agda.TypeChecking.SizedTypes.WarshallSolver
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, Agda.Compiler.Backend
listenToMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ListT
1 (Type/Class)	Agda.Utils.ListT
2 (Data Constructor)	Agda.Utils.ListT
ListTel	Agda.Syntax.Internal
ListTel'	Agda.Syntax.Internal
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.Syntax.Abstract
litBranches	Agda.TypeChecking.CompiledClause
litCase	Agda.TypeChecking.CompiledClause
LitChar	Agda.Syntax.Literal
litChar	Agda.Syntax.Parser.StringLiterals
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.MAlonzo.Compiler
3 (Function)	Agda.Compiler.JS.Compiler
literalsNotImplemented	Agda.Auto.Convert
literateExts	Agda.Syntax.Parser.Literate
literateExtsShortList	Agda.Syntax.Parser.Literate
literateMd	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
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.MAlonzo.Compiler
2 (Function)	Agda.Compiler.JS.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
litType	Agda.TypeChecking.Monad.Builtin
LoadedFileCache
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
loadFile	Agda.Interaction.CommandLine
Local
1 (Data Constructor)	Agda.Compiler.JS.Syntax
2 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
3 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
local	Agda.Compiler.JS.Compiler
LocalDisplayForm	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalId
1 (Type/Class)	Agda.Compiler.JS.Syntax
2 (Data Constructor)	Agda.Compiler.JS.Syntax
localLetBound	Agda.Syntax.Scope.Base
locally	Agda.Utils.Lens
localNameSpace	Agda.Syntax.Scope.Base
localScope	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localShadowedBy	Agda.Syntax.Scope.Base
localState	Agda.Utils.Monad
localStateCommandM	Agda.Interaction.InteractionTop
localTCState	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localTCStateSaving	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalTerminationEnv	Agda.Auto.CaseSplit
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, Agda.Compiler.Backend
loffset	Agda.TypeChecking.SizedTypes.WarshallSolver
LoneProjectionLike	Agda.TypeChecking.ProjectionLike
look	Agda.Utils.Parser.ReadP
LookAhead	Agda.Syntax.Parser.LookAhead
Lookup	Agda.Compiler.JS.Syntax
lookup
1 (Function)	Agda.Utils.BiMap
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.Trie
4 (Function)	Agda.Compiler.JS.Substitution
5 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
6 (Function)	Agda.Utils.AssocList
lookupBV	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupDefault	Agda.Utils.HashMap
lookupDefinition	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupEdge	Agda.TypeChecking.SizedTypes.WarshallSolver
lookupImportedName	Agda.Syntax.Scope.Monad
lookupIndex
1 (Function)	Agda.Utils.IndexedList
2 (Function)	Agda.Compiler.MAlonzo.Compiler
lookupInteractionId	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupInteractionMeta	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupInteractionMeta_	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupInteractionPoint	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMeta
1 (Function)	Agda.Syntax.Internal.Defs
2 (Function)	Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
3 (Function)	Agda.TypeChecking.Reduce.Monad
lookupModuleFromSource	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMutualBlock	Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupPath	Agda.Utils.Trie
lookupPatternSyn	Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupPrimitiveFunction	Agda.TypeChecking.Primitive
lookupPrimitiveFunctionQ	Agda.TypeChecking.Primitive
lookupS	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
lookupSection	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupTrie	Agda.Utils.Trie
lowerBounds	Agda.TypeChecking.SizedTypes.WarshallSolver
lowMetaPriority	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lparen	Agda.Utils.Pretty
lSnd	Agda.Utils.Lens
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