Agda-2.6.1.3: A dependently typed functional programming language and proof assistant

Index - L

L 
1 (Data Constructor)Agda.Auto.Options
2 (Data Constructor)Agda.Interaction.EmacsCommand
Label 
1 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Data Constructor)Agda.TypeChecking.SizedTypes.WarshallSolver
labelAgda.Utils.Graph.AdjacencyMap.Unidirectional
LabelledEdgeAgda.TypeChecking.SizedTypes.WarshallSolver
LabelPatVarsAgda.Syntax.Internal.Pattern
labelPatVarsAgda.Syntax.Internal.Pattern
Lam 
1 (Data Constructor)Agda.Auto.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Reflected
5 (Data Constructor)Agda.Syntax.Abstract
lamAgda.TypeChecking.Names
Lambda 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
lambdaAgda.Syntax.Concrete.Pretty
lambdaAddContextAgda.TypeChecking.Rules.Term
LambdaBoundAgda.Syntax.Scope.Base
lambdaCohesionCheckAgda.TypeChecking.Rules.Term
LambdaHoleAgda.Syntax.Notation
lambdaIrrelevanceCheckAgda.TypeChecking.Rules.Term
lambdaLiftExprAgda.Syntax.Abstract
lambdaModalityCheckAgda.TypeChecking.Rules.Term
lambdaQuantityCheckAgda.TypeChecking.Rules.Term
LamBinding 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
LamBinding'Agda.Syntax.Concrete
lamBindingsToTelescopeAgda.Syntax.Concrete
lamBracketsAgda.Syntax.Fixity
lamCatchAllAgda.Syntax.Concrete
LamClause 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
lamLHSAgda.Syntax.Concrete
LamNotPiAgda.TypeChecking.Rules.Term
LamOrPiAgda.TypeChecking.Rules.Term
lamRHSAgda.Syntax.Concrete
LamVAgda.Syntax.Concrete.Operators.Parser
LamView 
1 (Type/Class)Agda.Syntax.Abstract.Views
2 (Data Constructor)Agda.Syntax.Abstract.Views
lamViewAgda.Syntax.Abstract.Views
lamWhereAgda.Syntax.Concrete
LanguagePragmaAgda.Utils.Haskell.Syntax
largestAgda.TypeChecking.SizedTypes.WarshallSolver
last2Agda.Utils.List
lastMaybeAgda.Utils.List
LaTeXAgda.Interaction.Base
Layer 
1 (Type/Class)Agda.Syntax.Parser.Literate
2 (Data Constructor)Agda.Syntax.Parser.Literate
layerContentAgda.Syntax.Parser.Literate
LayerRoleAgda.Syntax.Parser.Literate
layerRoleAgda.Syntax.Parser.Literate
LayersAgda.Syntax.Parser.Literate
LayoutAgda.Syntax.Parser.Monad
layoutAgda.Syntax.Parser.Lexer
LayoutContextAgda.Syntax.Parser.Monad
layoutKeywordsAgda.Syntax.Parser.Tokens
LazyAgda.Utils.Haskell.Syntax
lazyAbsAppAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
LazyEvaluationAgda.Syntax.Treeless, Agda.Compiler.Backend
lazyMatchAgda.TypeChecking.CompiledClause
LazySplit 
1 (Type/Class)Agda.TypeChecking.Coverage.SplitTree
2 (Data Constructor)Agda.TypeChecking.Coverage.SplitTree
lblBindingsAgda.TypeChecking.Coverage.SplitTree
lblConstructorNameAgda.TypeChecking.Coverage.SplitTree
lblLazyAgda.TypeChecking.Coverage.SplitTree
lblSplitArgAgda.TypeChecking.Coverage.SplitTree
lbraceAgda.Utils.Pretty
lbrackAgda.Utils.Pretty
lcmpAgda.TypeChecking.SizedTypes.WarshallSolver
LeAgda.TypeChecking.SizedTypes.Syntax
leAgda.Termination.Order
LeastAgda.TypeChecking.SizedTypes.Syntax
LeaveSectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LeftAssocAgda.Syntax.Common
LeftClosedPOMonoidAgda.Utils.POMonoid
LeftDisjunctAgda.Auto.NarrowingSearch
leftExprAgda.TypeChecking.SizedTypes.Syntax
leftIdiomBrktAgda.Syntax.Concrete.Pretty
LeftModeAgda.Utils.Pretty
LeftOfArrowAgda.TypeChecking.Positivity.Occurrence
LeftOperandCtxAgda.Syntax.Fixity
LeftoverPatterns 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
LegendMatrix 
1 (Type/Class)Agda.Utils.Warshall
2 (Data Constructor)Agda.Utils.Warshall
LElAgda.TypeChecking.Rules.Data
Lens'Agda.Utils.Lens
lensAccumStatisticsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensAccumStatisticsPAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensAmodNameAgda.Syntax.Scope.Base
lensAnameNameAgda.Syntax.Scope.Base
LensArgInfoAgda.Syntax.Common
LensAttributeAgda.Syntax.Concrete.Attribute
LensClosureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensClosureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensCohesionAgda.Syntax.Common
LensCommandLineOptionsAgda.Interaction.Options.Lenses
LensConNameAgda.Syntax.Internal
lensField1Agda.Utils.Lens.Examples
lensField2Agda.Utils.Lens.Examples
LensFixityAgda.Syntax.Common
lensFixityAgda.Syntax.Common
LensFixity'Agda.Syntax.Common
lensFixity'Agda.Syntax.Common
LensFlexRigAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
lensFlexRigAgda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
LensFreeVariablesAgda.Syntax.Common
lensFreshAgda.TypeChecking.Serialise.Base
LensGetAgda.Utils.Lens
LensHidingAgda.Syntax.Common
LensIncludePathsAgda.Interaction.Options.Lenses
LensInScopeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
lensInScopeAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
LensIsAbstractAgda.Syntax.Common
lensIsAbstractAgda.Syntax.Common
lensLexInputAgda.Syntax.Parser.Alex
LensMapAgda.Utils.Lens
LensModalityAgda.Syntax.Common
LensNamedAgda.Syntax.Common
lensNamedAgda.Syntax.Common
LensOriginAgda.Syntax.Common
lensPersistentStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensPersistentVerbosityAgda.Interaction.Options.Lenses
LensPragmaOptionsAgda.Interaction.Options.Lenses
lensPragmaOptionsAgda.Interaction.Options.Lenses
lensQNameNameAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
LensQuantityAgda.Syntax.Common
LensRelevanceAgda.Syntax.Common
LensSafeModeAgda.Interaction.Options.Lenses
LensSetAgda.Utils.Lens
LensSortAgda.Syntax.Internal
lensSortAgda.Syntax.Internal
LensTCEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensTCEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensVerbosityAgda.Interaction.Options.Lenses
LeqAgda.TypeChecking.SizedTypes
leqConjAgda.TypeChecking.Conversion
leqIntervalAgda.TypeChecking.Conversion
leqLevelAgda.TypeChecking.Conversion
leqPOAgda.Utils.PartialOrd
leqSortAgda.TypeChecking.Conversion
leqTypeAgda.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
LetApplyAgda.Syntax.Abstract
LetBindAgda.Syntax.Abstract
LetBindingAgda.Syntax.Abstract
LetBindingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LetBoundAgda.Syntax.Scope.Base
LetDeclaredVariableAgda.Syntax.Abstract
LetInfoAgda.Syntax.Info
LetOpenAgda.Syntax.Abstract
LetOpenModuleAgda.Syntax.Scope.Monad
LetPatBindAgda.Syntax.Abstract
LetRangeAgda.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
Level'Agda.Syntax.Internal
LevelAtomAgda.Syntax.Internal
LevelAtom'Agda.Syntax.Internal
LevelCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LevelKit 
1 (Type/Class)Agda.TypeChecking.Level
2 (Data Constructor)Agda.TypeChecking.Level
levelLowerBoundAgda.TypeChecking.Level
levelLubAgda.TypeChecking.Substitute
levelMaxAgda.TypeChecking.Substitute
levelMaxDiffAgda.TypeChecking.Level
levelMaxViewAgda.TypeChecking.Level
levelPlusAgda.Syntax.Internal
levelPlusViewAgda.TypeChecking.Level
LevelReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LevelsAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
levelSucAgda.Syntax.Internal
levelSucFunctionAgda.TypeChecking.Level
levelTmAgda.TypeChecking.Substitute
levelTypeAgda.TypeChecking.Level
levelViewAgda.TypeChecking.Level
levelView'Agda.TypeChecking.Level
LexActionAgda.Syntax.Parser.Alex
lexerAgda.Syntax.Parser.Lexer
lexErrorAgda.Syntax.Parser.Monad, Agda.Syntax.Parser.LexActions
lexInputAgda.Syntax.Parser.Alex
lexPosAgda.Syntax.Parser.Alex
LexPredicateAgda.Syntax.Parser.Alex
lexPrevCharAgda.Syntax.Parser.Alex
lexSrcFileAgda.Syntax.Parser.Alex
LexStateAgda.Syntax.Parser.Monad
lexTokenAgda.Syntax.Parser.LexActions
lfcCachedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lfcCurrentAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lFstAgda.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
LHSAppP 
1 (Data Constructor)Agda.Syntax.Concrete.Pattern
2 (Data Constructor)Agda.Syntax.Abstract.Pattern
lhsAsBindingsAgda.TypeChecking.Rules.LHS
lhsBodyTypeAgda.TypeChecking.Rules.LHS
LHSCore 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
lhsCoreAgda.Syntax.Abstract
LHSCore'Agda.Syntax.Abstract
lhsCoreAddChunkAgda.Syntax.Abstract.Pattern
lhsCoreAddSpine 
1 (Function)Agda.Syntax.Concrete.Pattern
2 (Function)Agda.Syntax.Abstract.Pattern
lhsCoreAllPatternsAgda.Syntax.Abstract.Pattern
lhsCoreApp 
1 (Function)Agda.Syntax.Concrete.Pattern
2 (Function)Agda.Syntax.Abstract.Pattern
lhsCoreToPatternAgda.Syntax.Abstract.Pattern
lhsCoreToSpineAgda.Syntax.Abstract.Pattern
lhsCoreWith 
1 (Function)Agda.Syntax.Concrete.Pattern
2 (Function)Agda.Syntax.Abstract.Pattern
lhsDefName 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsDestructor 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsEllipsisAgda.Syntax.Info
lhsExpandedEllipsisAgda.Syntax.Concrete
lhsFocus 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsHasAbsurdAgda.TypeChecking.Rules.LHS
LHSHead 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
lhsHead 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
LHSInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
lhsInfoAgda.Syntax.Abstract
lhsOriginalPatternAgda.Syntax.Concrete
LHSOrPatSynAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lhsOutPatAgda.TypeChecking.Rules.LHS.Problem
lhsParametersAgda.TypeChecking.Rules.LHS
lhsPartialSplitAgda.TypeChecking.Rules.LHS
lhsPats 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsPatsLeftAgda.Syntax.Concrete
lhsPatSubstAgda.TypeChecking.Rules.LHS
lhsPatternsAgda.TypeChecking.Rules.LHS
LHSPatternView 
1 (Type/Class)Agda.Syntax.Concrete.Pattern
2 (Type/Class)Agda.Syntax.Abstract.Pattern
lhsPatternView 
1 (Function)Agda.Syntax.Concrete.Pattern
2 (Function)Agda.Syntax.Abstract.Pattern
lhsProblemAgda.TypeChecking.Rules.LHS.Problem
LHSProj 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
LHSProjPAgda.Syntax.Abstract.Pattern
lhsRangeAgda.Syntax.Info
LHSResult 
1 (Type/Class)Agda.TypeChecking.Rules.LHS
2 (Data Constructor)Agda.TypeChecking.Rules.LHS
lhsRewriteEqnAgda.Syntax.Concrete
LHSState 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
lhsTargetAgda.TypeChecking.Rules.LHS.Problem
lhsTelAgda.TypeChecking.Rules.LHS.Problem
LHSToSpineAgda.Syntax.Abstract.Pattern
lhsToSpineAgda.Syntax.Abstract.Pattern
lhsVarTeleAgda.TypeChecking.Rules.LHS
LHSWith 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
lhsWithExprAgda.Syntax.Concrete
LHSWithP 
1 (Data Constructor)Agda.Syntax.Concrete.Pattern
2 (Data Constructor)Agda.Syntax.Abstract.Pattern
lhsWithPatterns 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
libDependsAgda.Interaction.Library.Base
libFileAgda.Interaction.Library.Base
libFilePosAgda.Interaction.Library
libIncludesAgda.Interaction.Library.Base
LibMAgda.Interaction.Library
LibNameAgda.Interaction.Library.Base, Agda.Interaction.Library
libNameAgda.Interaction.Library.Base
libNameForCurrentDirAgda.Interaction.Library.Base
LibPositionInfo 
1 (Type/Class)Agda.Interaction.Library
2 (Data Constructor)Agda.Interaction.Library
libraryIncludePathsAgda.Interaction.Library
LibraryWarningAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
libraryWarningNameAgda.Interaction.Library
libToTCMAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LibUnknownField_Agda.Interaction.Options.Warnings
LibWarning 
1 (Type/Class)Agda.Interaction.Library
2 (Data Constructor)Agda.Interaction.Library
LibWarning'Agda.Interaction.Library.Parse
Lift 
1 (Type/Class)Agda.Auto.CaseSplit
2 (Data Constructor)Agda.Syntax.Internal, Agda.TypeChecking.Substitute
liftAgda.Auto.CaseSplit
lift'Agda.Auto.CaseSplit
liftCommandMTAgda.Interaction.InteractionTop
liftCommandMTLocalStateAgda.Interaction.InteractionTop
liftListTAgda.Utils.ListT
liftLocalStateAgda.Interaction.InteractionTop
liftP 
1 (Function)Agda.Utils.Permutation
2 (Function)Agda.Syntax.Parser.LookAhead
liftReduceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
liftSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
liftTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
liftU1Agda.TypeChecking.Unquote
liftU2Agda.TypeChecking.Unquote
lIndexAgda.Utils.IndexedList
lineLengthAgda.Utils.Pretty
LineNumberAgda.Interaction.Library.Parse
lineNumPosAgda.Interaction.Library
LInfAgda.TypeChecking.SizedTypes.WarshallSolver
LispAgda.Interaction.EmacsCommand
lispifyHighlightingInfoAgda.Interaction.Highlighting.Emacs
lispifyTokenBasedAgda.Interaction.Highlighting.Emacs
listAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
List2 
1 (Type/Class)Agda.Utils.Tuple
2 (Data Constructor)Agda.Utils.Tuple
list2Agda.Utils.Tuple
listCaseAgda.Utils.List
listenDirtyAgda.Utils.Update
ListenerAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
listenToMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
listSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
ListT 
1 (Type/Class)Agda.Utils.ListT
2 (Data Constructor)Agda.Utils.ListT
ListTelAgda.Syntax.Internal
listTelAgda.Syntax.Internal
ListTel'Agda.Syntax.Internal
listToMaybe 
1 (Function)Agda.Utils.Maybe
2 (Function)Agda.Utils.Maybe.Strict
ListZipAgda.Utils.Zipper
ListZipperAgda.Utils.Zipper
Lit 
1 (Data Constructor)Agda.Utils.Haskell.Syntax
2 (Data Constructor)Agda.Syntax.Concrete
3 (Data Constructor)Agda.Syntax.Internal
4 (Data Constructor)Agda.Syntax.Reflected
5 (Data Constructor)Agda.Syntax.Abstract
litBranchesAgda.TypeChecking.CompiledClause
litCaseAgda.TypeChecking.CompiledClause
LitCharAgda.Syntax.Literal
litCharAgda.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
literal'Agda.Syntax.Parser.LexActions
literalsNotImplementedAgda.Auto.Convert
literateExtsShortListAgda.Syntax.Parser.Literate
literateMdAgda.Syntax.Parser.Literate
literateOrgAgda.Syntax.Parser.Literate
literateProcessorsAgda.Syntax.Parser.Literate
literateRsTAgda.Syntax.Parser.Literate
literateSrcFileAgda.Syntax.Parser.Literate
literateTeXAgda.Syntax.Parser.Literate
LitFloatAgda.Syntax.Literal
LitMetaAgda.Syntax.Literal
LitNatAgda.Syntax.Literal
LitP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Reflected
4 (Data Constructor)Agda.Syntax.Abstract
litPAgda.Syntax.Internal
LitQNameAgda.Syntax.Literal
litqname 
1 (Function)Agda.Compiler.MAlonzo.Compiler
2 (Function)Agda.Compiler.JS.Compiler
litqnamepatAgda.Compiler.MAlonzo.Compiler
LitSAgda.Syntax.Reflected
LitStringAgda.Syntax.Literal
litString 
1 (Function)Agda.Syntax.Parser.StringLiterals
2 (Function)Agda.Compiler.MAlonzo.Compiler
litTypeAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LitWord64Agda.Syntax.Literal
lModCohesionAgda.Syntax.Common
lModQuantityAgda.Syntax.Common
lModRelevanceAgda.Syntax.Common
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
loadFileAgda.Interaction.CommandLine
LocalAgda.Compiler.JS.Syntax
localAgda.Compiler.JS.Compiler
localBindingSourceAgda.Syntax.Scope.Base
localCacheAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalDisplayFormAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalId 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
locallyAgda.Utils.Lens
locally'Agda.Utils.Lens
locallyScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
locallyStateAgda.Utils.Lens
locallyTCAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
locallyTCStateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localNameSpaceAgda.Syntax.Scope.Base
localRAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localShadowedByAgda.Syntax.Scope.Base
localStateAgda.Utils.Monad
localStateCommandMAgda.Interaction.InteractionTop
localTCAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localTCStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localTCStateSavingAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localTCStateSavingWarningsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalTerminationEnvAgda.Auto.CaseSplit
localTerminationEnvAgda.Auto.CaseSplit
localTerminationSidecondAgda.Auto.CaseSplit
localToAbstractAgda.Syntax.Translation.ConcreteToAbstract
LocalVAgda.Syntax.Concrete.Operators.Parser
LocalVar 
1 (Type/Class)Agda.Syntax.Scope.Base
2 (Data Constructor)Agda.Syntax.Scope.Base
localVarAgda.Syntax.Scope.Base
LocalVarsAgda.Syntax.Scope.Base
LocalVsImportedModuleClashAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
loffsetAgda.TypeChecking.SizedTypes.WarshallSolver
LoneProjectionLikeAgda.TypeChecking.ProjectionLike
LookAheadAgda.Syntax.Parser.LookAhead
lookAheadErrorAgda.Syntax.Parser.LookAhead
LookupAgda.Compiler.JS.Syntax
lookup 
1 (Function)Agda.Utils.AssocList
2 (Function)Agda.Utils.BiMap
3 (Function)Agda.Utils.Trie
4 (Function)Agda.Compiler.JS.Substitution
5 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
lookupBackendAgda.Compiler.Backend
lookupBVAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupBV'Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupDefinitionAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupEdgeAgda.TypeChecking.SizedTypes.WarshallSolver
lookupImportedNameAgda.Syntax.Scope.Monad
lookupIndex 
1 (Function)Agda.Utils.IndexedList
2 (Function)Agda.Compiler.MAlonzo.Compiler
lookupInteractionIdAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupInteractionMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupInteractionMeta_Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupInteractionPointAgda.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
lookupMeta'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupModuleFromSourceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupPathAgda.Utils.Trie
lookupPatternSynAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupPrimitiveFunctionAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
lookupPrimitiveFunctionQAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
lookupSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
lookupSectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupSinglePatternSynAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupTrieAgda.Utils.Trie
lookupVarMapAgda.TypeChecking.Free.Lazy
lowerBoundsAgda.TypeChecking.SizedTypes.WarshallSolver
lowMetaPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lparenAgda.Utils.Pretty
lSndAgda.Utils.Lens
LtAgda.TypeChecking.SizedTypes.Syntax
ltAgda.Termination.Order
ltrimAgda.Utils.String
LType 
1 (Data Constructor)Agda.TypeChecking.Rules.Data
2 (Type/Class)Agda.TypeChecking.Rules.Data
lTypeLevelAgda.TypeChecking.Rules.Data
lubAgda.TypeChecking.SizedTypes.WarshallSolver
lub'Agda.TypeChecking.SizedTypes.WarshallSolver
Lvl 
1 (Type/Class)Agda.TypeChecking.Primitive
2 (Data Constructor)Agda.TypeChecking.Primitive
lvlMaxAgda.TypeChecking.Level
lvlSucAgda.TypeChecking.Level
lvlTypeAgda.TypeChecking.Level
lvlZeroAgda.TypeChecking.Level