| 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 |