| L | |
| 1 (Data Constructor) | Agda.Interaction.EmacsCommand |
| 2 (Data Constructor) | Agda.Utils.Map |
| label | Agda.Utils.QuickCheck |
| labels | Agda.Utils.QuickCheck |
| Lam | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Internal |
| 4 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| Lambda | Agda.Compiler.JS.Syntax |
| lambda | |
| 1 (Function) | Agda.Compiler.JS.Case |
| 2 (Function) | Agda.Syntax.Concrete.Pretty |
| lambda' | Agda.Compiler.JS.Case |
| LambdaHole | Agda.Syntax.Notation |
| LamBinding | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| lamBrackets | Agda.Syntax.Fixity |
| lamFreq | Agda.TypeChecking.Test.Generators |
| LamNotPi | Agda.TypeChecking.Rules.Term |
| LamOrPi | Agda.TypeChecking.Rules.Term |
| LamV | Agda.Syntax.Concrete.Operators.Parser |
| Layout | Agda.Syntax.Parser.Monad |
| layout | Agda.Syntax.Parser.Lexer |
| LayoutContext | Agda.Syntax.Parser.Monad |
| layoutKeywords | Agda.Syntax.Parser.Tokens |
| Lazy | Agda.Compiler.Epic.AuxAST |
| lazy | Agda.Compiler.Epic.AuxAST |
| lbrace | Agda.Utils.Pretty |
| lbrack | Agda.Utils.Pretty |
| LChar | Agda.Compiler.Epic.AuxAST |
| le | Agda.Termination.CallGraph |
| leaveTopLevel | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| LeftAssoc | Agda.Syntax.Fixity |
| LeftDisjunct | Agda.Auto.NarrowingSearch |
| leftDistributive | Agda.Utils.TestHelpers |
| LeftHandSide | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| leftHH | Agda.TypeChecking.Rules.LHS.Unify |
| LeftMode | Agda.Utils.Pretty |
| LeftOfArrow | Agda.TypeChecking.Positivity |
| LeftOperandCtx | Agda.Syntax.Fixity |
| LegendMatrix | |
| 1 (Type/Class) | Agda.Utils.Warshall |
| 2 (Data Constructor) | Agda.Utils.Warshall |
| Leq | Agda.TypeChecking.SizedTypes |
| leqLevel | Agda.TypeChecking.Conversion |
| leqSort | Agda.TypeChecking.Conversion |
| leqType | Agda.TypeChecking.Conversion |
| leqType_ | Agda.TypeChecking.Rules.Term |
| Let | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| LetApply | Agda.Syntax.Abstract |
| LetBind | Agda.Syntax.Abstract |
| LetBinding | Agda.Syntax.Abstract |
| LetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| LetDef | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| LetDefs | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| LetInfo | Agda.Syntax.Info |
| LetOpen | Agda.Syntax.Abstract |
| LetRange | Agda.Syntax.Info |
| lett | Agda.Compiler.Epic.AuxAST |
| Level | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| LevelAtom | Agda.Syntax.Internal |
| LevelCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| LevelKit | |
| 1 (Type/Class) | Agda.TypeChecking.Level |
| 2 (Data Constructor) | Agda.TypeChecking.Level |
| levelLub | Agda.TypeChecking.Level |
| levelMax | Agda.TypeChecking.Substitute |
| Levels | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| levelSort | Agda.TypeChecking.Substitute |
| levelSuc | Agda.Syntax.Internal |
| levelSucFunction | Agda.TypeChecking.Level |
| levelTm | Agda.TypeChecking.Substitute |
| levelView | Agda.TypeChecking.Level |
| LexAction | Agda.Syntax.Parser.Alex |
| lexer | Agda.Syntax.Parser.Lexer |
| lexError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser.LexActions |
| lexInput | Agda.Syntax.Parser.Alex |
| LexOrder | Agda.Termination.Lexicographic |
| lexOrder | Agda.Termination.Lexicographic |
| lexPos | Agda.Syntax.Parser.Alex |
| LexPredicate | Agda.Syntax.Parser.Alex |
| lexPrevChar | Agda.Syntax.Parser.Alex |
| LexState | Agda.Syntax.Parser.Monad |
| lexToken | Agda.Syntax.Parser.LexActions |
| LFloat | Agda.Compiler.Epic.AuxAST |
| 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 |
| LHSInfo | Agda.Syntax.Info |
| lhsOriginalPattern | Agda.Syntax.Concrete |
| LHSRange | Agda.Syntax.Info |
| lhsRewriteEqn | Agda.Syntax.Concrete |
| lhsWithExpr | Agda.Syntax.Concrete |
| lhsWithPattern | Agda.Syntax.Concrete |
| lift | Agda.Auto.CaseSplit |
| liftEither | Agda.Utils.Monad |
| liftP | Agda.Syntax.Parser.LookAhead |
| liftTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| lineLength | Agda.Utils.Pretty |
| LInt | Agda.Compiler.Epic.AuxAST |
| Lisp | Agda.Interaction.EmacsCommand |
| list | Agda.TypeChecking.Primitive |
| Listener | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| listenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| listOf | Agda.Utils.QuickCheck |
| listOf1 | Agda.Utils.QuickCheck |
| listOfElements | Agda.Utils.TestHelpers |
| listToMaybe | Agda.Utils.Maybe |
| Lit | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 4 (Type/Class) | Agda.Compiler.Epic.AuxAST |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| litBranches | Agda.TypeChecking.CompiledClause |
| litCase | Agda.TypeChecking.CompiledClause |
| LitChar | Agda.Syntax.Literal |
| litChar | Agda.Syntax.Parser.StringLiterals |
| litCon | Agda.Compiler.Epic.Injection |
| Literal | Agda.Syntax.Literal |
| literal | |
| 1 (Function) | Agda.Syntax.Parser.LexActions |
| 2 (Function) | Agda.Compiler.MAlonzo.Compiler |
| 3 (Function) | Agda.Compiler.JS.Compiler |
| literate | Agda.Syntax.Parser.Lexer |
| LitFloat | Agda.Syntax.Literal |
| LitFocus | Agda.TypeChecking.Rules.LHS.Problem |
| litFreq | Agda.TypeChecking.Test.Generators |
| LitInt | Agda.Syntax.Literal |
| LitMP | Agda.TypeChecking.Coverage.Match |
| LitP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| LitQName | Agda.Syntax.Literal |
| litqname | Agda.Compiler.MAlonzo.Compiler |
| LitSh | Agda.TypeChecking.Rules.LHS.Unify |
| LitString | Agda.Syntax.Literal |
| litString | Agda.Syntax.Parser.StringLiterals |
| litToCon | Agda.Compiler.Epic.Injection |
| litType | Agda.TypeChecking.Rules.Term |
| loadFile | Agda.Interaction.CommandLine.CommandLine |
| Local | Agda.Compiler.JS.Syntax |
| LocalId | |
| 1 (Type/Class) | Agda.Compiler.JS.Syntax |
| 2 (Data Constructor) | Agda.Compiler.JS.Syntax |
| localid | Agda.Compiler.JS.Parser |
| localNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| localScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| localState | Agda.TypeChecking.Constraints |
| localTerminationEnv | Agda.Auto.CaseSplit |
| localTerminationSidecond | Agda.Auto.CaseSplit |
| localToAbstract | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| LocalV | Agda.Syntax.Concrete.Operators.Parser |
| LocalVars | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| LocalVsImportedModuleClash | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| look | Agda.Utils.ReadP |
| LookAhead | Agda.Syntax.Parser.LookAhead |
| lookInterface | Agda.Compiler.Epic.CompileState |
| Lookup | Agda.Compiler.JS.Syntax |
| lookup | |
| 1 (Function) | Agda.Utils.Graph |
| 2 (Function) | Agda.Compiler.JS.Substitution |
| lookupEdge | Agda.Utils.Warshall |
| lookupInteractionId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| lookupMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| lookupMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| lookupPath | Agda.Utils.Trie |
| lookupPrimitiveFunction | Agda.TypeChecking.Primitive |
| lookupSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| LowerMeta | Agda.Interaction.GhciTop |
| lowerMeta | Agda.Interaction.GhciTop |
| lowMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| lparen | Agda.Utils.Pretty |
| LString | Agda.Compiler.Epic.AuxAST |
| lt | Agda.Termination.CallGraph |
| 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 |
| lvlView | Agda.TypeChecking.Substitute |
| lvlZero | Agda.TypeChecking.Level |