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

- 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.Interaction.EmacsCommand
2 (Data Constructor) | Agda.Mimer.Options
Label |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.WarshallSolver
label | Agda.Utils.Graph.AdjacencyMap.Unidirectional
LabelledEdge | Agda.TypeChecking.SizedTypes.WarshallSolver
LabelPatVars | Agda.Syntax.Internal.Pattern
labelPatVars | Agda.Syntax.Internal.Pattern
Lam |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Concrete
4 (Data Constructor) | Agda.Syntax.Abstract
lam | Agda.TypeChecking.Names
Lambda |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Compiler.JS.Syntax
lambda | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
lambdaAddContext | Agda.TypeChecking.Rules.Term
lambdaAnnotationCheck | Agda.TypeChecking.Rules.Term
LambdaBound | Agda.Syntax.Scope.Base
lambdaCohesionCheck | Agda.TypeChecking.Rules.Term
LambdaHole | Agda.Syntax.Notation
lambdaIrrelevanceCheck | Agda.TypeChecking.Rules.Term
LambdaIsErased | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LambdaIsErased_ | Agda.Interaction.Options.Errors
lambdaLiftExpr | Agda.Syntax.Abstract
lambdaModalityCheck | Agda.TypeChecking.Rules.Term
lambdaPolarityCheck | Agda.TypeChecking.Rules.Term
lambdaQuantityCheck | Agda.TypeChecking.Rules.Term
LamBinding |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
LamBinding' | Agda.Syntax.Concrete
lamBindings | Agda.Syntax.Parser.Helpers
lamBindingsToTelescope | Agda.Syntax.Concrete
LamBinds |
1 (Type/Class) | Agda.Syntax.Parser.Helpers
2 (Data Constructor) | Agda.Syntax.Parser.Helpers
LamBinds' | Agda.Syntax.Parser.Helpers
lamBrackets | Agda.Syntax.Fixity
lamCatchall | Agda.Syntax.Concrete
LamClause |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
lamLHS | Agda.Syntax.Concrete
LamNotPi | Agda.TypeChecking.Rules.Term
LamOrPi | Agda.TypeChecking.Rules.Term
lamRHS | Agda.Syntax.Concrete
lamTel | Agda.TypeChecking.Names
LamV | Agda.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
Language | Agda.Syntax.Common
LanguagePragma | Agda.Utils.Haskell.Syntax
LargeSort | Agda.TypeChecking.Substitute
largest | Agda.TypeChecking.SizedTypes.WarshallSolver
last | Agda.Utils.List1
last1 | Agda.Utils.List
last2 |
1 (Function) | Agda.Utils.List
2 (Function) | Agda.Utils.List1
last2' | Agda.Utils.List
lastIdPart | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
lastMaybe | Agda.Utils.List
lastWithDefault | Agda.Utils.List
LaTeX | Agda.Interaction.Base
latexBackend | Agda.Interaction.Highlighting.LaTeX.Backend, Agda.Interaction.Highlighting.LaTeX
latexOptCountClusters | Agda.Interaction.Highlighting.LaTeX.Base
LaTeXOptions |
1 (Type/Class) | Agda.Interaction.Highlighting.LaTeX.Base
2 (Data Constructor) | Agda.Interaction.Highlighting.LaTeX.Base
latexOptOutDir | Agda.Interaction.Highlighting.LaTeX.Base
latexOptSourceFileName | Agda.Interaction.Highlighting.LaTeX.Base
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
LayoutBlock | Agda.Syntax.Parser.Monad
LayoutContext | Agda.Syntax.Parser.Monad
layoutKeywords | Agda.Syntax.Parser.Tokens
LayoutStatus | Agda.Syntax.Parser.Monad
Lazy | Agda.Utils.Haskell.Syntax
lazyAbsApp | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
LazyEvaluation | Agda.Syntax.Treeless, Agda.Compiler.Backend
lazyMatch | Agda.TypeChecking.CompiledClause
LazySplit |
1 (Type/Class) | Agda.TypeChecking.Coverage.SplitTree
2 (Data Constructor) | Agda.TypeChecking.Coverage.SplitTree
lblBindings | Agda.TypeChecking.Coverage.SplitTree
lblConstructorName | Agda.TypeChecking.Coverage.SplitTree
lblLazy | Agda.TypeChecking.Coverage.SplitTree
lblSplitArg | Agda.TypeChecking.Coverage.SplitTree
lbrace | Agda.Syntax.Common.Pretty
lbrack | Agda.Syntax.Common.Pretty
lcmp | Agda.TypeChecking.SizedTypes.WarshallSolver
Le | Agda.TypeChecking.SizedTypes.Syntax
le | Agda.Termination.Order
Least | Agda.TypeChecking.SizedTypes.Syntax
LeaveSection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LeftAssoc | Agda.Syntax.Common
LeftClosedPOMonoid | Agda.Utils.POMonoid
leftExpr | Agda.TypeChecking.SizedTypes.Syntax
leftIdiomBrkt | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
LeftLet | Agda.Syntax.Common
LeftMode | Agda.Syntax.Common.Pretty
LeftOfArrow | Agda.TypeChecking.Positivity.Occurrence
LeftOperandCtx | Agda.Syntax.Fixity
LeftoverPatterns |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem
lefts | Agda.Utils.List1
LEl | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
length | Agda.Utils.List1
lens | Agda.Utils.Lens
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
LensAnnotation | Agda.Syntax.Common
lensAreWeCaching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensArgInfo | Agda.Syntax.Common
LensAttribute | Agda.Syntax.Concrete.Attribute
lensAwakeConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensBackends | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensBenchmark | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensBuiltinModuleIds | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensClosure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensClosure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensCohesion | Agda.Syntax.Common
lensCollapseDefault | Agda.Utils.WithDefault
LensCommandLineOptions | Agda.Interaction.Options.Lenses
lensConcreteNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensConfigAbove | Agda.Interaction.Library.Base
LensConName | Agda.Syntax.Internal
lensConsideringInstance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensCopiedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensDirty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensDisambiguatedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensEqTel | Agda.TypeChecking.Rules.LHS.Unify.Types
lensField1 | Agda.Utils.Lens.Examples
lensField2 | Agda.Utils.Lens.Examples
lensFileDict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFileDictBuilder | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFileDictBuiltinModuleIds | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFileDictFileDictBuilder | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFileDictPrimitiveLibDir | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensFixity | Agda.Syntax.Common
lensFixity | Agda.Syntax.Common
LensFixity' | Agda.Syntax.Common
lensFixity' | Agda.Syntax.Common
LensFlexRig | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
lensFlexRig | Agda.TypeChecking.Free.Lazy, Agda.TypeChecking.Free
lensForeignCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensFreeVariables | Agda.Syntax.Common
lensFresh | Agda.TypeChecking.Serialise.Base
lensFreshCheckpointId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFreshInt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFreshInteractionId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFreshMetaId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFreshMutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFreshNameId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFreshOpaqueId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFreshProblemId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensGet | Agda.Utils.Lens
lensHead | Agda.Utils.List1
LensHiding | Agda.Syntax.Common
lensImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensImportedDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensImportedMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensImportedModulesTransitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensImportedPartialDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensImportedUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensImportsDisplayForms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensIncludePaths | Agda.Interaction.Options.Lenses
LensInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
lensInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
lensInstanceHack | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensInstantiateBlocking | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensIsAbstract | Agda.Syntax.Common
lensIsAbstract | Agda.Syntax.Common
LensIsOpaque | Agda.Syntax.Common
lensIsOpaque | Agda.Syntax.Common
lensKeepDefault | Agda.Utils.WithDefault
lensLast | Agda.Utils.List1
lensLexInput | Agda.Syntax.Parser.Alex
lensLibCache | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensLoadedFileCache | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensLocalPartialDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensLocalUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensLock | Agda.Syntax.Common
LensMap | Agda.Utils.Lens
lensMaybeLazy | Agda.Utils.Maybe.Strict
LensModality | Agda.Syntax.Common
LensModalPolarity | Agda.Syntax.Common
lensModuleCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensModuleToSourceId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensNameCopies | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensNamed | Agda.Syntax.Common
lensNamed | Agda.Syntax.Common
lensNameId | Agda.Syntax.Concrete.Definitions.Monad
lensNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
lensOccursCheckDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensOpaqueBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensOpaqueIds | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensOpenMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensOptAllowExec | Agda.Interaction.Options
lensOptAllowIncompleteMatch | Agda.Interaction.Options
lensOptAllowUnsolved | Agda.Interaction.Options
lensOptAutoInline | Agda.Interaction.Options
lensOptBacktrackingInstances | Agda.Interaction.Options
lensOptCaching | Agda.Interaction.Options
lensOptCallByName | Agda.Interaction.Options
lensOptCohesion | Agda.Interaction.Options
lensOptCompileMain | Agda.Interaction.Options
lensOptConfluenceCheck | Agda.Interaction.Options
lensOptCopatterns | Agda.Interaction.Options
lensOptCountClusters | Agda.Interaction.Options
lensOptCubical | Agda.Interaction.Options
lensOptCubicalCompatible | Agda.Interaction.Options
lensOptCumulativity | Agda.Interaction.Options
lensOptDoubleCheck | Agda.Interaction.Options
lensOptErasedMatches | Agda.Interaction.Options
lensOptEraseRecordParameters | Agda.Interaction.Options
lensOptErasure | Agda.Interaction.Options
lensOptEta | Agda.Interaction.Options
lensOptExactSplit | Agda.Interaction.Options
lensOptExperimentalIrrelevance | Agda.Interaction.Options
lensOptExperimentalLazyInstances | Agda.Interaction.Options
lensOptFastReduce | Agda.Interaction.Options
lensOptFirstOrder | Agda.Interaction.Options
lensOptFlatSplit | Agda.Interaction.Options
lensOptForcing | Agda.Interaction.Options
lensOptGuarded | Agda.Interaction.Options
lensOptGuardedness | Agda.Interaction.Options
lensOptHiddenArgumentPuns | Agda.Interaction.Options
lensOptImportSorts | Agda.Interaction.Options
lensOptInferAbsurdClauses | Agda.Interaction.Options
lensOptInjectiveTypeConstructors | Agda.Interaction.Options
lensOptInstanceSearchDepth | Agda.Interaction.Options
lensOptInversionMaxDepth | Agda.Interaction.Options
lensOptIrrelevantProjections | Agda.Interaction.Options
lensOptKeepCoveringClauses | Agda.Interaction.Options
lensOptKeepPatternVariables | Agda.Interaction.Options
lensOptLevelUniverse | Agda.Interaction.Options
lensOptLoadPrimitives | Agda.Interaction.Options
lensOptNoUniverseCheck | Agda.Interaction.Options
lensOptOmegaInOmega | Agda.Interaction.Options
lensOptPatternMatching | Agda.Interaction.Options
lensOptPolarity | Agda.Interaction.Options
lensOptPositivityCheck | Agda.Interaction.Options
lensOptPostfixProjections | Agda.Interaction.Options
lensOptPrintPatternSynonyms | Agda.Interaction.Options
lensOptProfiling | Agda.Interaction.Options
lensOptProjectionLike | Agda.Interaction.Options
lensOptProp | Agda.Interaction.Options
lensOptQualifiedInstances | Agda.Interaction.Options
lensOptRequireUniqueMetaSolutions | Agda.Interaction.Options
lensOptRewriting | Agda.Interaction.Options
lensOptSafe | Agda.Interaction.Options
lensOptSaveMetas | Agda.Interaction.Options
lensOptShowIdentitySubstitutions | Agda.Interaction.Options
lensOptShowImplicit | Agda.Interaction.Options
lensOptShowIrrelevant | Agda.Interaction.Options
lensOptSizedTypes | Agda.Interaction.Options
lensOptSyntacticEquality | Agda.Interaction.Options
lensOptTerminationCheck | Agda.Interaction.Options
lensOptTerminationDepth | Agda.Interaction.Options
lensOptTwoLevel | Agda.Interaction.Options
lensOptUniverseCheck | Agda.Interaction.Options
lensOptUniversePolymorphism | Agda.Interaction.Options
lensOptUseUnicode | Agda.Interaction.Options
lensOptVerbose | Agda.Interaction.Options
lensOptWarningMode | Agda.Interaction.Options
lensOptWithoutK | Agda.Interaction.Options
LensOrigin | Agda.Syntax.Common
lensOverlapMode | Agda.Syntax.Common
lensPairModuleToSource | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensPatternSynImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensPatternSyns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensPersistentSession | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensPersistentState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensPersistentVerbosity | Agda.Interaction.Options.Lenses
lensPostponeInstanceSearch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensPostScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensPragmaOptions | Agda.Interaction.Options
lensPragmaOptions | Agda.Interaction.Options
lensPreScopeState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensPreTokens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensPrimitiveLibDir | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensProduct | Agda.Utils.Lens
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
LensQuantity | Agda.Syntax.Common
lensRecEta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensRecTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensRelevance | Agda.Syntax.Common
LensSafeMode | Agda.Interaction.Options.Lenses
lensScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensSessionState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensSet | Agda.Utils.Lens
lensShadowingNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensSingleWarning | Agda.Interaction.Options.Warnings
lensSleepingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensSolvedMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensSort | Agda.Syntax.Internal
lensSort | Agda.Syntax.Internal
lensStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensSyntaxInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LensTCEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensTCEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensTCWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensTemporaryInstances | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensTheDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensTopLevelModuleNameParts | Agda.Syntax.TopLevelModuleName
lensTopLevelModuleNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensUsedNames | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensVarTel | Agda.TypeChecking.Rules.LHS.Unify.Types
LensVerbosity | Agda.Interaction.Options.Lenses
lensVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lensWarningOnImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Leq | Agda.TypeChecking.SizedTypes
leqConj | Agda.TypeChecking.Conversion
leqInterval | Agda.TypeChecking.Conversion
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
LetAxiom | Agda.Syntax.Abstract
LetBind | Agda.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
LetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LetBound | Agda.Syntax.Scope.Base
LetExpressions | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LetInfo | Agda.Syntax.Info
LetOpen | Agda.Syntax.Abstract
LetOpenModule | Agda.Syntax.Scope.Monad
letOrigin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LetPatBind | Agda.Syntax.Abstract
LetRange | Agda.Syntax.Info
letTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
letType | Agda.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
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
levelLowerBound | Agda.TypeChecking.Level
levelLub | Agda.TypeChecking.Substitute
levelMax | Agda.TypeChecking.Substitute
levelMaxDiff | Agda.TypeChecking.Level
levelMaxView | Agda.TypeChecking.Level
levelPlus | Agda.Syntax.Internal
levelPlusView | Agda.TypeChecking.Level
LevelReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Levels | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
levelSuc | Agda.Syntax.Internal
levelTm | Agda.TypeChecking.Substitute
levelType | Agda.TypeChecking.Level
levelType' | Agda.TypeChecking.Level
LevelUniv | Agda.Syntax.Internal
levelView | Agda.TypeChecking.Level
levelView' | Agda.TypeChecking.Level
LexAction |
1 (Type/Class) | Agda.Syntax.Parser.Alex
2 (Data Constructor) | 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
lfExists | Agda.Interaction.Library.Base
lfPath | Agda.Interaction.Library.Base
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
LHSAppP |
1 (Data Constructor) | Agda.Syntax.Concrete.Pattern
2 (Data Constructor) | Agda.Syntax.Abstract.Pattern
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
lhsCoreAddChunk | Agda.Syntax.Abstract.Pattern
lhsCoreAddSpine |
1 (Function) | Agda.Syntax.Concrete.Pattern
2 (Function) | Agda.Syntax.Abstract.Pattern
lhsCoreAllPatterns | Agda.Syntax.Abstract.Pattern
lhsCoreApp |
1 (Function) | Agda.Syntax.Concrete.Pattern
2 (Function) | Agda.Syntax.Abstract.Pattern
lhsCoreToPattern | Agda.Syntax.Abstract.Pattern
lhsCoreToSpine | Agda.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
LHSEllipsis | Agda.Syntax.Concrete
lhsEllipsis | Agda.Syntax.Info
lhsEllipsisPat | Agda.Syntax.Concrete
lhsEllipsisRange | Agda.Syntax.Concrete
lhsFocus |
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract
lhsHasAbsurd | Agda.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
lhsIndexedSplit | Agda.TypeChecking.Rules.LHS
LHSInfo |
1 (Type/Class) | Agda.Syntax.Info
2 (Data Constructor) | Agda.Syntax.Info
lhsInfo | Agda.Syntax.Abstract
LHSNotDefinitionOrConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lhsOriginalPattern | Agda.Syntax.Concrete
LHSOrPatSyn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lhsOutPat | Agda.TypeChecking.Rules.LHS.Problem
lhsParameters | Agda.TypeChecking.Rules.LHS
lhsPartialSplit | Agda.TypeChecking.Rules.LHS
lhsPats |
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract
lhsPatsLeft | Agda.Syntax.Concrete
lhsPatSubst | Agda.TypeChecking.Rules.LHS
lhsPatterns | Agda.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
lhsProblem | Agda.TypeChecking.Rules.LHS.Problem
LHSProj |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
LHSProjP | Agda.Syntax.Abstract.Pattern
lhsRange | Agda.Syntax.Info
LHSReduces | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LHSResult |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS
lhsRewriteEqn | Agda.Syntax.Concrete
LHSState |
1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem
lhsTarget | Agda.TypeChecking.Rules.LHS.Problem
lhsTel | Agda.TypeChecking.Rules.LHS.Problem
LHSToSpine | Agda.Syntax.Abstract.Pattern
lhsToSpine | Agda.Syntax.Abstract.Pattern
lhsVarTele | Agda.TypeChecking.Rules.LHS
LHSWith |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
lhsWithExpr | Agda.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
libAbove | Agda.Interaction.Library.Base
LibCache |
1 (Type/Class) | Agda.Interaction.Library.Base
2 (Data Constructor) | Agda.Interaction.Library.Base
libDepends | Agda.Interaction.Library.Base
LibError |
1 (Type/Class) | Agda.Interaction.Library.Base
2 (Data Constructor) | Agda.Interaction.Library.Base
LibError' | Agda.Interaction.Library.Base
LibErrorIO | Agda.Interaction.Library.Base
LibErrors |
1 (Type/Class) | Agda.Interaction.Library.Base
2 (Data Constructor) | Agda.Interaction.Library.Base
libErrors | Agda.Interaction.Library.Base
libErrorsInstalledLibraries | Agda.Interaction.Library.Base
LibErrWarns | Agda.Interaction.Library.Base
libFile | Agda.Interaction.Library.Base
libFilePos | Agda.Interaction.Library.Base, Agda.Interaction.Library
libIncludes | Agda.Interaction.Library.Base
LibM | Agda.Interaction.Library.Base, Agda.Interaction.Library
LibName |
1 (Type/Class) | Agda.Interaction.Library.Base, Agda.Interaction.Library
2 (Data Constructor) | Agda.Interaction.Library.Base
libName | Agda.Interaction.Library.Base
libNameBase | Agda.Interaction.Library.Base
libNameForCurrentDir | Agda.Interaction.Library.Base
libNameVersion | Agda.Interaction.Library.Base
LibNotFound | Agda.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
libPragmas | Agda.Interaction.Library.Base
LibrariesFile |
1 (Type/Class) | Agda.Interaction.Library.Base
2 (Data Constructor) | Agda.Interaction.Library.Base
LibrariesFileNotFound | Agda.Interaction.Library.Base
LibraryError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LibraryError_ | Agda.Interaction.Options.Errors
libraryIncludePaths | Agda.Interaction.Library
LibraryWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
libraryWarningName | Agda.Interaction.Library.Base, Agda.Interaction.Library
LibState | Agda.Interaction.Library.Base
LibTooFarDown | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LibTooFarDown_ | Agda.Interaction.Options.Errors
libToTCM | Agda.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
Lift | Agda.Syntax.Internal, Agda.TypeChecking.Substitute
lift | Agda.Utils.Monad
liftA2 | Agda.Utils.Monad
liftA4 | Agda.Utils.Applicative
liftCommandMT | Agda.Interaction.InteractionTop
liftCommandMTLocalState | Agda.Interaction.InteractionTop
liftList1 | Agda.Utils.List1
liftListT | Agda.Utils.ListT
liftLocalState | Agda.Interaction.Command
liftM2 | Agda.Utils.Monad
liftM3 | Agda.Utils.Monad
liftM4 | Agda.Utils.Monad
liftMaybe | Agda.Utils.Maybe
liftOmitField | Agda.Interaction.JSON
liftOmitField2 | Agda.Interaction.JSON
liftOmittedField | Agda.Interaction.JSON
liftOmittedField2 | Agda.Interaction.JSON
liftP |
1 (Function) | Agda.Utils.Permutation
2 (Function) | Agda.Syntax.Parser.LookAhead
liftParseJSON | Agda.Interaction.JSON
liftParseJSON2 | Agda.Interaction.JSON
liftParseJSONList | Agda.Interaction.JSON
liftParseJSONList2 | Agda.Interaction.JSON
liftReduce | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
liftS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
liftTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
liftToEncoding | Agda.Interaction.JSON
liftToEncoding2 | Agda.Interaction.JSON
liftToEncodingList | Agda.Interaction.JSON
liftToEncodingList2 | Agda.Interaction.JSON
liftToJSON | Agda.Interaction.JSON
liftToJSON2 | Agda.Interaction.JSON
liftToJSONList | Agda.Interaction.JSON
liftToJSONList2 | Agda.Interaction.JSON
liftU1 | Agda.TypeChecking.Unquote
liftU2 | Agda.TypeChecking.Unquote
lIndex | Agda.Utils.IndexedList
lineLength | Agda.Syntax.Common.Pretty
LineNumber | Agda.Interaction.Library.Base
lineNumPos | Agda.Interaction.Library.Base, Agda.Interaction.Library
LInf | Agda.TypeChecking.SizedTypes.WarshallSolver
Lisp | Agda.Interaction.EmacsCommand
lispifyHighlightingInfo | Agda.Interaction.Highlighting.Emacs
lispifyTokenBased | Agda.Interaction.Highlighting.Emacs
list | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
List1 | Agda.Utils.List1
List2 |
1 (Type/Class) | Agda.Utils.List2
2 (Data Constructor) | Agda.Utils.List2
listArray | Agda.Utils.IArray
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
listS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
ListT |
1 (Type/Class) | Agda.Utils.ListT
2 (Data Constructor) | Agda.Utils.ListT
ListTel | Agda.Syntax.Internal
listTel | Agda.Syntax.Internal
ListTel' | Agda.Syntax.Internal
listToMaybe |
1 (Function) | Agda.Utils.Maybe
2 (Function) | Agda.Utils.Maybe.Strict
ListZip | Agda.Utils.Zipper
ListZipper | Agda.Utils.Zipper
Lit |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Reflected
4 (Data Constructor) | Agda.Syntax.Concrete
5 (Data Constructor) | Agda.Syntax.Abstract
litBranches | Agda.TypeChecking.CompiledClause
litCase | Agda.TypeChecking.CompiledClause
LitChar | Agda.Syntax.Literal
litChar | Agda.Syntax.Parser.StringLiterals
LitConflict | Agda.TypeChecking.Rules.LHS.Unify.Types
litConflictAt | Agda.TypeChecking.Rules.LHS.Unify.Types
litConflictLeft | Agda.TypeChecking.Rules.LHS.Unify.Types
litConflictRight | Agda.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
LiteralTooBig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LiteralTooBig_ | Agda.Interaction.Options.Errors
literateExtsShortList | Agda.Syntax.Parser.Literate
literateMd | Agda.Syntax.Parser.Literate
literateOrg | Agda.Syntax.Parser.Literate
literateProcessors | Agda.Syntax.Parser.Literate
literateRsT | Agda.Syntax.Parser.Literate
literateTeX | Agda.Syntax.Parser.Literate
LitFloat | Agda.Syntax.Literal
LitMeta | Agda.Syntax.Literal
litmeta | Agda.Compiler.JS.Compiler
LitNat | Agda.Syntax.Literal
LitP |
1 (Data Constructor) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Concrete
4 (Data Constructor) | Agda.Syntax.Abstract
litP | Agda.Syntax.Internal
LitQName | Agda.Syntax.Literal
litqname | Agda.Compiler.JS.Compiler
LitS | Agda.Syntax.Reflected
LitString | Agda.Syntax.Literal
litString | Agda.Syntax.Parser.StringLiterals
litType |
1 (Function) | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function) | Agda.TypeChecking.Rules.LHS.Unify.Types
LitWord64 | Agda.Syntax.Literal
LM | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
lModCohesion | Agda.Syntax.Common
lModPolarity | Agda.Syntax.Common
lModQuantity | Agda.Syntax.Common
lModRelevance | Agda.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
Local | Agda.Compiler.JS.Syntax
local | Agda.Compiler.JS.Compiler
LocalBind | Agda.Utils.Haskell.Syntax
localBindingSource | Agda.Syntax.Scope.Base
localCache | Agda.TypeChecking.Monad.Caching, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalCandidate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalConfluenceCheck | Agda.Interaction.Options
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
LocalK | Agda.TypeChecking.DiscrimTree.Types
locally | Agda.Utils.Lens
locally' | Agda.Utils.Lens
locallyReconstructed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
locallyReduceAllDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
locallyReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
locallyScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
locallyState | Agda.Utils.Lens
locallyTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
locallyTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LocalMetaStore | Agda.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
localNames | Agda.Syntax.Scope.Flat
localNameSpace | Agda.Syntax.Scope.Base
localR | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localShadowedBy | Agda.Syntax.Scope.Base
localState | Agda.Utils.Monad
localStateCommandM | Agda.Interaction.Command
localTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localTCState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localTCStateSaving | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
localTCStateSavingWarnings | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
locatedTypeError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
locateFlag | Agda.Setup.EmacsMode
Lock | Agda.Syntax.Common
LockAttribute | Agda.Syntax.Concrete.Attribute
lockAttributeTable | Agda.Syntax.Concrete.Attribute
LockOLock | Agda.Syntax.Common
LockOrigin | Agda.Syntax.Common
LockOTick | Agda.Syntax.Common
LockUniv | Agda.Syntax.Internal
loffset | Agda.TypeChecking.SizedTypes.WarshallSolver
logHtml | Agda.Interaction.Highlighting.HTML.Base
LogHtmlT | Agda.Interaction.Highlighting.HTML.Base
logLaTeX | Agda.Interaction.Highlighting.LaTeX.Base
LogMessage |
1 (Type/Class) | Agda.Interaction.Highlighting.LaTeX.Base
2 (Data Constructor) | Agda.Interaction.Highlighting.LaTeX.Base
logMsgToText | Agda.Interaction.Highlighting.LaTeX.Base
LoneConstructor | Agda.Syntax.Concrete
loneFuns | Agda.Syntax.Concrete.Definitions.Monad
LoneProjectionLike | Agda.TypeChecking.ProjectionLike
LoneSig |
1 (Type/Class) | Agda.Syntax.Concrete.Definitions.Monad
2 (Data Constructor) | Agda.Syntax.Concrete.Definitions.Monad
loneSigKind | Agda.Syntax.Concrete.Definitions.Monad
loneSigName | Agda.Syntax.Concrete.Definitions.Monad
loneSigRange | Agda.Syntax.Concrete.Definitions.Monad
LoneSigs | Agda.Syntax.Concrete.Definitions.Monad
loneSigs | Agda.Syntax.Concrete.Definitions.Monad
loneSigsFromLoneNames | Agda.Syntax.Concrete.Definitions.Monad
longestPaths | Agda.Utils.Graph.AdjacencyMap.Unidirectional
LookAhead | Agda.Syntax.Parser.LookAhead
lookAheadError | Agda.Syntax.Parser.LookAhead
Lookup | Agda.Compiler.JS.Syntax
lookup |
1 (Function) | Agda.Utils.AssocList
2 (Function) | Agda.Utils.Map1
3 (Function) | Agda.Utils.HashTable
4 (Function) | Agda.Utils.Trie
5 (Function) | Agda.Utils.BiMap
6 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
7 (Function) | Agda.Compiler.JS.Substitution
lookupBackend | Agda.TypeChecking.Monad.State, 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
lookupBV_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupDefinition | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupDT | Agda.TypeChecking.DiscrimTree
lookupEdge | Agda.TypeChecking.SizedTypes.WarshallSolver
lookupGE |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
lookupGT |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
lookupImportedName | Agda.Syntax.Scope.Monad
lookupIndex |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
3 (Function) | Agda.Utils.IndexedList
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
lookupLE |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
lookupLocalMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupLocalMeta' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupLT |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
lookupME | Agda.TypeChecking.Serialise.Base
lookupMeta |
1 (Function) | Agda.Syntax.Internal.Defs
2 (Function) | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMetaInstantiation | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMetaJudgement | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMetaModality | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupMin | Agda.Utils.BoolSet
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.Base, Agda.TypeChecking.Primitive
lookupPrimitiveFunctionQ | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
lookupS | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
lookupSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupSinglePatternSyn | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupTrie | Agda.Utils.Trie
lookupUnifyDT | Agda.TypeChecking.DiscrimTree
lookupVarMap | Agda.TypeChecking.Free.Lazy
lowerBounds | Agda.TypeChecking.SizedTypes.WarshallSolver
lowMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lparen | Agda.Syntax.Common.Pretty
lSnd | Agda.Utils.Lens
Lt | Agda.TypeChecking.SizedTypes.Syntax
lt | Agda.Termination.Order
lTextC | Agda.TypeChecking.Serialise.Base
lTextD | Agda.TypeChecking.Serialise.Base
lTextE | Agda.TypeChecking.Serialise.Base
ltrim | Agda.Utils.String
LType |
1 (Data Constructor) | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
2 (Type/Class) | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
lTypeLevel | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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
lvlZero | Agda.TypeChecking.Level