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.Concrete |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Syntax.Reflected |
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 |
lambdaLiftExpr | Agda.Syntax.Abstract |
lambdaModalityCheck | 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 |
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 |
LegendMatrix | |
1 (Type/Class) | Agda.Utils.Warshall |
2 (Data Constructor) | Agda.Utils.Warshall |
LEl | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
length | Agda.Utils.List1 |
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 |
LensArgInfo | Agda.Syntax.Common |
LensAttribute | Agda.Syntax.Concrete.Attribute |
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 |
LensConName | Agda.Syntax.Internal |
lensConstructor | 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 |
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 |
LensFreeVariables | Agda.Syntax.Common |
lensFresh | Agda.TypeChecking.Serialise.Base |
lensFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
LensGet | Agda.Utils.Lens |
lensHead | Agda.Utils.List1 |
LensHiding | Agda.Syntax.Common |
LensIncludePaths | Agda.Interaction.Options.Lenses |
LensInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
lensInScope | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
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 |
LensLock | Agda.Syntax.Common |
LensMap | Agda.Utils.Lens |
LensModality | Agda.Syntax.Common |
LensNamed | Agda.Syntax.Common |
lensNamed | Agda.Syntax.Common |
lensNameId | Agda.Syntax.Concrete.Definitions.Monad |
lensNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
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 |
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 |
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 |
lensPersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
LensPersistentVerbosity | Agda.Interaction.Options.Lenses |
LensPragmaOptions | Agda.Interaction.Options.Lenses |
lensPragmaOptions | Agda.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 |
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 |
LensSet | Agda.Utils.Lens |
lensSingleWarning | Agda.Interaction.Options.Warnings |
LensSort | Agda.Syntax.Internal |
lensSort | Agda.Syntax.Internal |
LensTCEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
lensTCEnv | 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 |
lensVarTel | Agda.TypeChecking.Rules.LHS.Unify.Types |
LensVerbosity | Agda.Interaction.Options.Lenses |
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 |
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 |
LetDeclaredVariable | Agda.Syntax.Abstract |
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 |
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 | Agda.Interaction.Library.Base, Agda.Interaction.Library |
libName | Agda.Interaction.Library.Base |
libNameForCurrentDir | 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 |
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 |
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 |
liftCommandMT | Agda.Interaction.InteractionTop |
liftCommandMTLocalState | Agda.Interaction.InteractionTop |
liftList1 | Agda.Utils.List1 |
liftListT | Agda.Utils.ListT |
liftLocalState | Agda.Interaction.InteractionTop |
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.Concrete |
3 (Data Constructor) | Agda.Syntax.Internal |
4 (Data Constructor) | Agda.Syntax.Reflected |
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 |
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 |
literateSrcFile | 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.Concrete |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Syntax.Reflected |
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 |
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.InteractionTop |
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 |
LocalVsImportedModuleClash | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
locatedTypeError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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.HashTable |
3 (Function) | Agda.Utils.Trie |
4 (Function) | Agda.Utils.BiMap |
5 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
6 (Function) | Agda.Compiler.JS.Substitution |
lookupBackend | 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 |
lookupImportedName | Agda.Syntax.Scope.Monad |
lookupIndex | 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 |
lookupLocalMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
lookupLocalMeta' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
lookupQName | Agda.Syntax.Translation.AbstractToConcrete |
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 |