Agda-2.6.2.0.20211129: 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.Glyph, Agda.Syntax.Concrete.Pretty
lambdaAddContextAgda.TypeChecking.Rules.Term
lambdaAnnotationCheckAgda.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
lamView 
1 (Function)Agda.Syntax.Abstract.Views
2 (Function)Agda.TypeChecking.Substitute
LanguageAgda.Syntax.Common
LanguagePragmaAgda.Utils.Haskell.Syntax
largestAgda.TypeChecking.SizedTypes.WarshallSolver
lastAgda.Utils.List1
last1Agda.Utils.List
last2Agda.Utils.List
lastIdPartAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
lastMaybeAgda.Utils.List
lastWithDefaultAgda.Utils.List
LaTeXAgda.Interaction.Base
latexBackendAgda.Interaction.Highlighting.LaTeX
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
LayoutBlockAgda.Syntax.Parser.Monad
LayoutContextAgda.Syntax.Parser.Monad
layoutKeywordsAgda.Syntax.Parser.Tokens
LayoutStatusAgda.Syntax.Parser.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
LeftAssocAgda.Syntax.Common
LeftClosedPOMonoidAgda.Utils.POMonoid
LeftDisjunctAgda.Auto.NarrowingSearch
leftExprAgda.TypeChecking.SizedTypes.Syntax
leftIdiomBrktAgda.Syntax.Concrete.Glyph, Agda.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
leftsAgda.Utils.List1
LegendMatrix 
1 (Type/Class)Agda.Utils.Warshall
2 (Data Constructor)Agda.Utils.Warshall
LElAgda.TypeChecking.Rules.Data
lengthAgda.Utils.List1
Lens'Agda.Utils.Lens
lensAccumStatisticsAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
lensAccumStatisticsPAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
lensAmodNameAgda.Syntax.Scope.Base
lensAnameNameAgda.Syntax.Scope.Base
LensAnnotationAgda.Syntax.Common
LensArgInfoAgda.Syntax.Common
LensAttributeAgda.Syntax.Concrete.Attribute
LensClosureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
lensClosureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
LensLockAgda.Syntax.Common
LensMapAgda.Utils.Lens
LensModalityAgda.Syntax.Common
LensNamedAgda.Syntax.Common
lensNamedAgda.Syntax.Common
lensNameIdAgda.Syntax.Concrete.Definitions.Monad
lensNamePartsAgda.Syntax.Concrete.Name, Agda.Syntax.Concrete
LensOriginAgda.Syntax.Common
lensPersistentStateAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
LensPersistentVerbosityAgda.Interaction.Options.Lenses
LensPragmaOptionsAgda.Interaction.Options.Lenses
lensPragmaOptionsAgda.Interaction.Options.Lenses
lensQNameName 
1 (Function)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function)Agda.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.Compiler.Backend, Agda.TypeChecking.Monad
lensTCEnvAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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
LevelCmpAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
LevelsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
levelSucAgda.Syntax.Internal
levelSucFunctionAgda.TypeChecking.Level
levelTmAgda.TypeChecking.Substitute
levelTypeAgda.TypeChecking.Level
levelViewAgda.TypeChecking.Level
levelView'Agda.TypeChecking.Level
LexAction 
1 (Type/Class)Agda.Syntax.Parser.Alex
2 (Data Constructor)Agda.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.Compiler.Backend, Agda.TypeChecking.Monad
lfcCurrentAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
lfExistsAgda.Interaction.Library.Base
lfPathAgda.Interaction.Library.Base
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.Concrete
lhsEllipsisAgda.Syntax.Info
lhsEllipsisPatAgda.Syntax.Concrete
lhsEllipsisRangeAgda.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.Compiler.Backend, Agda.TypeChecking.Monad
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
LibError 
1 (Type/Class)Agda.Interaction.Library.Base
2 (Data Constructor)Agda.Interaction.Library.Base
LibError'Agda.Interaction.Library.Base
LibErrorIOAgda.Interaction.Library.Base
libFileAgda.Interaction.Library.Base
libFilePosAgda.Interaction.Library.Base, Agda.Interaction.Library
libIncludesAgda.Interaction.Library.Base
LibMAgda.Interaction.Library.Base, Agda.Interaction.Library
LibNameAgda.Interaction.Library.Base, Agda.Interaction.Library
libNameAgda.Interaction.Library.Base
libNameForCurrentDirAgda.Interaction.Library.Base
LibNotFoundAgda.Interaction.Library.Base
LibPositionInfo 
1 (Type/Class)Agda.Interaction.Library.Base, Agda.Interaction.Library
2 (Data Constructor)Agda.Interaction.Library.Base, Agda.Interaction.Library
libPragmasAgda.Interaction.Library.Base
LibrariesFile 
1 (Type/Class)Agda.Interaction.Library.Base
2 (Data Constructor)Agda.Interaction.Library.Base
libraryIncludePathsAgda.Interaction.Library
LibraryWarningAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
libraryWarningNameAgda.Interaction.Library.Base, Agda.Interaction.Library
LibStateAgda.Interaction.Library.Base
libToTCMAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
LibUnknownField_Agda.Interaction.Options.Warnings
LibWarning 
1 (Type/Class)Agda.Interaction.Library.Base, Agda.Interaction.Library
2 (Data Constructor)Agda.Interaction.Library.Base, Agda.Interaction.Library
LibWarning'Agda.Interaction.Library.Base
Lift 
1 (Type/Class)Agda.Auto.CaseSplit
2 (Data Constructor)Agda.Syntax.Internal, Agda.TypeChecking.Substitute
liftAgda.Auto.CaseSplit
lift'Agda.Auto.CaseSplit
liftCCAgda.Compiler.MAlonzo.Compiler
liftCommandMTAgda.Interaction.InteractionTop
liftCommandMTLocalStateAgda.Interaction.InteractionTop
liftListTAgda.Utils.ListT
liftLocalStateAgda.Interaction.InteractionTop
liftMaybeAgda.Utils.Maybe
liftP 
1 (Function)Agda.Utils.Permutation
2 (Function)Agda.Syntax.Parser.LookAhead
liftParseJSONAgda.Interaction.JSON
liftParseJSON2Agda.Interaction.JSON
liftParseJSONListAgda.Interaction.JSON
liftParseJSONList2Agda.Interaction.JSON
liftReduceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
liftSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
liftTCMAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
liftToEncodingAgda.Interaction.JSON
liftToEncoding2Agda.Interaction.JSON
liftToEncodingListAgda.Interaction.JSON
liftToEncodingList2Agda.Interaction.JSON
liftToJSONAgda.Interaction.JSON
liftToJSON2Agda.Interaction.JSON
liftToJSONListAgda.Interaction.JSON
liftToJSONList2Agda.Interaction.JSON
liftU1Agda.TypeChecking.Unquote
liftU2Agda.TypeChecking.Unquote
lIndexAgda.Utils.IndexedList
lineLengthAgda.Utils.Pretty
LineNumberAgda.Interaction.Library.Base
lineNumPosAgda.Interaction.Library.Base, Agda.Interaction.Library
LInfAgda.TypeChecking.SizedTypes.WarshallSolver
LispAgda.Interaction.EmacsCommand
lispifyHighlightingInfoAgda.Interaction.Highlighting.Emacs
lispifyTokenBasedAgda.Interaction.Highlighting.Emacs
listAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
List1Agda.Utils.List1
List2 
1 (Type/Class)Agda.Utils.List2
2 (Data Constructor)Agda.Utils.List2
listCaseAgda.Utils.List
listenDirtyAgda.Utils.Update
ListenerAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
listenToMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
LitWord64Agda.Syntax.Literal
lModCohesionAgda.Syntax.Common
lModQuantityAgda.Syntax.Common
lModRelevanceAgda.Syntax.Common
LoadedFileCache 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
LocalAgda.Compiler.JS.Syntax
localAgda.Compiler.JS.Compiler
LocalBindAgda.Utils.Haskell.Syntax
localBindingSourceAgda.Syntax.Scope.Base
localCacheAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Caching
LocalCandidateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
LocalConfluenceCheckAgda.Interaction.Options
LocalDisplayFormAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
LocalId 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
locallyAgda.Utils.Lens
locally'Agda.Utils.Lens
locallyReconstructedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
locallyReduceAllDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
locallyReduceDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
locallyScopeAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
locallyStateAgda.Utils.Lens
locallyTCAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
locallyTCStateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
localNameSpaceAgda.Syntax.Scope.Base
localRAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
localScopeAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
localShadowedByAgda.Syntax.Scope.Base
localStateAgda.Utils.Monad
localStateCommandMAgda.Interaction.InteractionTop
localTCAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
localTCStateAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
localTCStateSavingAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
localTCStateSavingWarningsAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
locatedTypeErrorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
LockAgda.Syntax.Common
LockAttributeAgda.Syntax.Concrete.Attribute
lockAttributeTableAgda.Syntax.Concrete.Attribute
LockUnivAgda.Syntax.Internal
loffsetAgda.TypeChecking.SizedTypes.WarshallSolver
LoneConstructorAgda.Syntax.Concrete
loneFunsAgda.Syntax.Concrete.Definitions.Monad
LoneProjectionLikeAgda.TypeChecking.ProjectionLike
LoneSig 
1 (Type/Class)Agda.Syntax.Concrete.Definitions.Monad
2 (Data Constructor)Agda.Syntax.Concrete.Definitions.Monad
loneSigKindAgda.Syntax.Concrete.Definitions.Monad
loneSigNameAgda.Syntax.Concrete.Definitions.Monad
loneSigRangeAgda.Syntax.Concrete.Definitions.Monad
LoneSigsAgda.Syntax.Concrete.Definitions.Monad
loneSigsAgda.Syntax.Concrete.Definitions.Monad
loneSigsFromLoneNamesAgda.Syntax.Concrete.Definitions.Monad
longestPathsAgda.Utils.Graph.AdjacencyMap.Unidirectional
LookAheadAgda.Syntax.Parser.LookAhead
lookAheadErrorAgda.Syntax.Parser.LookAhead
LookupAgda.Compiler.JS.Syntax
lookup 
1 (Function)Agda.Utils.AssocList
2 (Function)Agda.Utils.Trie
3 (Function)Agda.Utils.BiMap
4 (Function)Agda.Compiler.JS.Substitution
5 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
lookupBackendAgda.Compiler.Backend
lookupBVAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
lookupBV'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
lookupDefinitionAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
lookupEdgeAgda.TypeChecking.SizedTypes.WarshallSolver
lookupImportedNameAgda.Syntax.Scope.Monad
lookupIndex 
1 (Function)Agda.Utils.IndexedList
2 (Function)Agda.Compiler.MAlonzo.Compiler
lookupInteractionIdAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
lookupInteractionMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
lookupInteractionMeta_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
lookupInteractionPointAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
lookupMeta 
1 (Function)Agda.Syntax.Internal.Defs
2 (Function)Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
lookupMeta'Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
lookupModuleFromSourceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
lookupMutualBlockAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Mutual
lookupPathAgda.Utils.Trie
lookupPatternSynAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
lookupPrimitiveFunctionAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
lookupPrimitiveFunctionQAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
lookupQNameAgda.Syntax.Translation.AbstractToConcrete
lookupSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
lookupSectionAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
lookupSinglePatternSynAgda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
lookupTrieAgda.Utils.Trie
lookupVarMapAgda.TypeChecking.Free.Lazy
lowerBoundsAgda.TypeChecking.SizedTypes.WarshallSolver
lowMetaPriorityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
lparenAgda.Utils.Pretty
lSndAgda.Utils.Lens
LtAgda.TypeChecking.SizedTypes.Syntax
ltAgda.Termination.Order
lTextCAgda.TypeChecking.Serialise.Base
lTextDAgda.TypeChecking.Serialise.Base
lTextEAgda.TypeChecking.Serialise.Base
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