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

Index - L

L 
1 (Data Constructor)Agda.Interaction.EmacsCommand
2 (Data Constructor)Agda.Mimer.Options
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.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Reflected
4 (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
lamBindingsAgda.Syntax.Parser.Helpers
lamBindingsToTelescopeAgda.Syntax.Concrete
LamBinds 
1 (Type/Class)Agda.Syntax.Parser.Helpers
2 (Data Constructor)Agda.Syntax.Parser.Helpers
LamBinds'Agda.Syntax.Parser.Helpers
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
lamTelAgda.TypeChecking.Names
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
LargeSortAgda.TypeChecking.Substitute
largestAgda.TypeChecking.SizedTypes.WarshallSolver
lastAgda.Utils.List1
last1Agda.Utils.List
last2 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
last2'Agda.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.Syntax.Common.Pretty
lbrackAgda.Syntax.Common.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
leftExprAgda.TypeChecking.SizedTypes.Syntax
leftIdiomBrktAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
LeftLetAgda.Syntax.Common
LeftModeAgda.Syntax.Common.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.Primitive.Cubical, Agda.TypeChecking.Primitive
lengthAgda.Utils.List1
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
LensAnnotationAgda.Syntax.Common
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
lensCollapseDefaultAgda.Utils.WithDefault
LensCommandLineOptionsAgda.Interaction.Options.Lenses
LensConNameAgda.Syntax.Internal
lensConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensEqTelAgda.TypeChecking.Rules.LHS.Unify.Types
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
lensFunctionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensGetAgda.Utils.Lens
lensHeadAgda.Utils.List1
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
LensIsOpaqueAgda.Syntax.Common
lensIsOpaqueAgda.Syntax.Common
lensKeepDefaultAgda.Utils.WithDefault
lensLastAgda.Utils.List1
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
lensOptAllowExecAgda.Interaction.Options
lensOptAllowIncompleteMatchAgda.Interaction.Options
lensOptAllowUnsolvedAgda.Interaction.Options
lensOptAutoInlineAgda.Interaction.Options
lensOptBacktrackingInstancesAgda.Interaction.Options
lensOptCachingAgda.Interaction.Options
lensOptCallByNameAgda.Interaction.Options
lensOptCohesionAgda.Interaction.Options
lensOptCompileMainAgda.Interaction.Options
lensOptConfluenceCheckAgda.Interaction.Options
lensOptCopatternsAgda.Interaction.Options
lensOptCountClustersAgda.Interaction.Options
lensOptCubicalAgda.Interaction.Options
lensOptCubicalCompatibleAgda.Interaction.Options
lensOptCumulativityAgda.Interaction.Options
lensOptDoubleCheckAgda.Interaction.Options
lensOptErasedMatchesAgda.Interaction.Options
lensOptEraseRecordParametersAgda.Interaction.Options
lensOptErasureAgda.Interaction.Options
lensOptEtaAgda.Interaction.Options
lensOptExactSplitAgda.Interaction.Options
lensOptExperimentalIrrelevanceAgda.Interaction.Options
lensOptFastReduceAgda.Interaction.Options
lensOptFirstOrderAgda.Interaction.Options
lensOptFlatSplitAgda.Interaction.Options
lensOptForcingAgda.Interaction.Options
lensOptGuardedAgda.Interaction.Options
lensOptGuardednessAgda.Interaction.Options
lensOptHiddenArgumentPunsAgda.Interaction.Options
lensOptImportSortsAgda.Interaction.Options
lensOptInferAbsurdClausesAgda.Interaction.Options
lensOptInjectiveTypeConstructorsAgda.Interaction.Options
lensOptInstanceSearchDepthAgda.Interaction.Options
lensOptInversionMaxDepthAgda.Interaction.Options
lensOptIrrelevantProjectionsAgda.Interaction.Options
lensOptKeepCoveringClausesAgda.Interaction.Options
lensOptKeepPatternVariablesAgda.Interaction.Options
lensOptLevelUniverseAgda.Interaction.Options
lensOptLoadPrimitivesAgda.Interaction.Options
lensOptNoUniverseCheckAgda.Interaction.Options
lensOptOmegaInOmegaAgda.Interaction.Options
lensOptPatternMatchingAgda.Interaction.Options
lensOptPositivityCheckAgda.Interaction.Options
lensOptPostfixProjectionsAgda.Interaction.Options
lensOptPrintPatternSynonymsAgda.Interaction.Options
lensOptProfilingAgda.Interaction.Options
lensOptProjectionLikeAgda.Interaction.Options
lensOptPropAgda.Interaction.Options
lensOptQualifiedInstancesAgda.Interaction.Options
lensOptRequireUniqueMetaSolutionsAgda.Interaction.Options
lensOptRewritingAgda.Interaction.Options
lensOptSafeAgda.Interaction.Options
lensOptSaveMetasAgda.Interaction.Options
lensOptShowIdentitySubstitutionsAgda.Interaction.Options
lensOptShowImplicitAgda.Interaction.Options
lensOptShowIrrelevantAgda.Interaction.Options
lensOptSizedTypesAgda.Interaction.Options
lensOptSyntacticEqualityAgda.Interaction.Options
lensOptTerminationCheckAgda.Interaction.Options
lensOptTerminationDepthAgda.Interaction.Options
lensOptTwoLevelAgda.Interaction.Options
lensOptUniverseCheckAgda.Interaction.Options
lensOptUniversePolymorphismAgda.Interaction.Options
lensOptUseUnicodeAgda.Interaction.Options
lensOptVerboseAgda.Interaction.Options
lensOptWarningModeAgda.Interaction.Options
lensOptWithoutKAgda.Interaction.Options
LensOriginAgda.Syntax.Common
lensOverlapModeAgda.Syntax.Common
lensPersistentStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
lensRecEtaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensRecordAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensRecTelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensRelevanceAgda.Syntax.Common
LensSafeModeAgda.Interaction.Options.Lenses
LensSetAgda.Utils.Lens
lensSingleWarningAgda.Interaction.Options.Warnings
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
lensTheDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensTopLevelModuleNamePartsAgda.Syntax.TopLevelModuleName
lensVarTelAgda.TypeChecking.Rules.LHS.Unify.Types
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
LetBinding 
1 (Type/Class)Agda.Syntax.Abstract
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
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
letOriginAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LetPatBindAgda.Syntax.Abstract
LetRangeAgda.Syntax.Info
letTermAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
letTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Level 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
3 (Data Constructor)Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
4 (Type/Class)Agda.Interaction.Highlighting.Generate
Level'Agda.Syntax.Internal
LevelAtomAgda.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
levelTmAgda.TypeChecking.Substitute
levelTypeAgda.TypeChecking.Level
levelType'Agda.TypeChecking.Level
LevelUnivAgda.Syntax.Internal
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.TypeChecking.Monad, Agda.Compiler.Backend
lfcCurrentAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
lhsIndexedSplitAgda.TypeChecking.Rules.LHS
LHSInfo 
1 (Type/Class)Agda.Syntax.Info
2 (Data Constructor)Agda.Syntax.Info
lhsInfoAgda.Syntax.Abstract
LHSNotDefinitionOrConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
LHSReducesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
libAboveAgda.Interaction.Library.Base
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
LibErrors 
1 (Type/Class)Agda.Interaction.Library.Base
2 (Data Constructor)Agda.Interaction.Library.Base
libErrorsAgda.Interaction.Library.Base
libErrorsInstalledLibrariesAgda.Interaction.Library.Base
LibErrWarnsAgda.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
LibParseError 
1 (Type/Class)Agda.Interaction.Library.Base
2 (Data Constructor)Agda.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
LibrariesFileNotFoundAgda.Interaction.Library.Base
LibraryErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
libraryIncludePathsAgda.Interaction.Library
LibraryWarningAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
libraryWarningNameAgda.Interaction.Library.Base, Agda.Interaction.Library
LibStateAgda.Interaction.Library.Base
libToTCMAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
LiftAgda.Syntax.Internal, Agda.TypeChecking.Substitute
liftCommandMTAgda.Interaction.InteractionTop
liftCommandMTLocalStateAgda.Interaction.InteractionTop
liftList1Agda.Utils.List1
liftListTAgda.Utils.ListT
liftLocalStateAgda.Interaction.InteractionTop
liftMaybeAgda.Utils.Maybe
liftOmitFieldAgda.Interaction.JSON
liftOmitField2Agda.Interaction.JSON
liftOmittedFieldAgda.Interaction.JSON
liftOmittedField2Agda.Interaction.JSON
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.TypeChecking.Monad, Agda.Compiler.Backend
liftSAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
liftTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Common.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.Base, Agda.TypeChecking.Primitive
List1Agda.Utils.List1
List2 
1 (Type/Class)Agda.Utils.List2
2 (Data Constructor)Agda.Utils.List2
listArrayAgda.Utils.IArray
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
LitConflictAgda.TypeChecking.Rules.LHS.Unify.Types
litConflictAtAgda.TypeChecking.Rules.LHS.Unify.Types
litConflictLeftAgda.TypeChecking.Rules.LHS.Unify.Types
litConflictRightAgda.TypeChecking.Rules.LHS.Unify.Types
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
literal'Agda.Syntax.Parser.LexActions
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
litmetaAgda.Compiler.JS.Compiler
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
litqnameAgda.Compiler.JS.Compiler
LitSAgda.Syntax.Reflected
LitStringAgda.Syntax.Literal
litStringAgda.Syntax.Parser.StringLiterals
litType 
1 (Function)Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)Agda.TypeChecking.Rules.LHS.Unify.Types
LitWord64Agda.Syntax.Literal
LMAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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
LocalAgda.Compiler.JS.Syntax
localAgda.Compiler.JS.Compiler
LocalBindAgda.Utils.Haskell.Syntax
localBindingSourceAgda.Syntax.Scope.Base
localCacheAgda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalCandidateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalConfluenceCheckAgda.Interaction.Options
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
LocalKAgda.TypeChecking.DiscrimTree.Types
locallyAgda.Utils.Lens
locally'Agda.Utils.Lens
locallyReconstructedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
locallyReduceAllDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
locallyReduceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
LocalMetaStoreAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalMetaStores 
1 (Type/Class)Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localNamesAgda.Syntax.Scope.Flat
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
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
locatedTypeErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LockAgda.Syntax.Common
LockAttributeAgda.Syntax.Concrete.Attribute
lockAttributeTableAgda.Syntax.Concrete.Attribute
LockOLockAgda.Syntax.Common
LockOriginAgda.Syntax.Common
LockOTickAgda.Syntax.Common
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.HashTable
3 (Function)Agda.Utils.Trie
4 (Function)Agda.Utils.BiMap
5 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
6 (Function)Agda.Compiler.JS.Substitution
lookupBackendAgda.Compiler.Backend
lookupBVAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupBV'Agda.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
lookupDTAgda.TypeChecking.DiscrimTree
lookupEdgeAgda.TypeChecking.SizedTypes.WarshallSolver
lookupImportedNameAgda.Syntax.Scope.Monad
lookupIndexAgda.Utils.IndexedList
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
lookupLocalMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupLocalMeta'Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMEAgda.TypeChecking.Serialise.Base
lookupMeta 
1 (Function)Agda.Syntax.Internal.Defs
2 (Function)Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMetaInstantiationAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMetaJudgementAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMetaModalityAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMinAgda.Utils.BoolSet
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
lookupQNameAgda.Syntax.Translation.AbstractToConcrete
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
lookupUnifyDTAgda.TypeChecking.DiscrimTree
lookupVarMapAgda.TypeChecking.Free.Lazy
lowerBoundsAgda.TypeChecking.SizedTypes.WarshallSolver
lowMetaPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lparenAgda.Syntax.Common.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.Primitive.Cubical, Agda.TypeChecking.Primitive
2 (Type/Class)Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
lTypeLevelAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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