L | |
1 (Data Constructor) | Agda.Utils.Map |
2 (Data Constructor) | Agda.Interaction.GhciTop |
label | Agda.Utils.QuickCheck |
labels | Agda.Utils.QuickCheck |
Lam | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
3 (Data Constructor) | Agda.Syntax.Concrete |
4 (Data Constructor) | Agda.Syntax.Internal |
5 (Data Constructor) | Agda.Syntax.Abstract |
lambda | Agda.Syntax.Concrete.Pretty |
LambdaHole | Agda.Syntax.Notation |
lambdaLift | Agda.Compiler.Epic.LambdaLift |
lambdaLiftExpr | Agda.Compiler.Epic.LambdaLift |
lambdaLiftFun | Agda.Compiler.Epic.LambdaLift |
LamBinding | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Abstract |
lamBrackets | Agda.Syntax.Fixity |
lamFreq | Agda.TypeChecking.Test.Generators |
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 |
lbrace | Agda.Utils.Pretty |
lbrack | Agda.Utils.Pretty |
LChar | Agda.Compiler.Epic.AuxAST |
le | Agda.Termination.CallGraph |
LeftAssoc | Agda.Syntax.Fixity |
LeftDisjunct | Agda.Auto.NarrowingSearch |
leftDistributive | Agda.Utils.TestHelpers |
LeftHandSide | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
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 |
Let | |
1 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
2 (Data Constructor) | Agda.Syntax.Concrete |
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 |
LevelAtom | Agda.TypeChecking.Level |
LevelCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
LevelKit | |
1 (Type/Class) | Agda.TypeChecking.Level |
2 (Data Constructor) | Agda.TypeChecking.Level |
levelMax | Agda.TypeChecking.Level |
Levels | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
levelSuc | Agda.TypeChecking.Level |
levelSucFunction | Agda.TypeChecking.Level |
levelType | Agda.TypeChecking.Level |
LevelView | Agda.TypeChecking.Level |
levelView | Agda.TypeChecking.Level |
levelZero | 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 |
LHSRange | Agda.Syntax.Info |
lift | Agda.Auto.CaseSplit |
lift2 | Agda.Compiler.Epic.Forcing |
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.GhciTop |
list | Agda.TypeChecking.Primitive |
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.Compiler.Epic.AuxAST |
2 (Type/Class) | Agda.Compiler.Epic.AuxAST |
3 (Data Constructor) | Agda.Syntax.Concrete |
4 (Data Constructor) | Agda.Syntax.Internal |
5 (Data Constructor) | Agda.Syntax.Abstract |
litBranches | Agda.TypeChecking.CompiledClause |
litCase | Agda.TypeChecking.CompiledClause |
LitChar | Agda.Syntax.Literal |
litChar | Agda.Syntax.Parser.StringLiterals |
Literal | Agda.Syntax.Literal |
literal | |
1 (Function) | Agda.Syntax.Parser.LexActions |
2 (Function) | Agda.Compiler.MAlonzo.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 |
LitLevel | 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 |
LitString | Agda.Syntax.Literal |
litString | Agda.Syntax.Parser.StringLiterals |
litType | Agda.TypeChecking.Rules.Term |
LL | Agda.Compiler.Epic.LambdaLift |
loadFile | Agda.Interaction.CommandLine.CommandLine |
localNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
localScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
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 |
lookup | Agda.Utils.Graph |
lookupConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
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 |
Lub | Agda.Syntax.Internal |
Lvl | |
1 (Type/Class) | Agda.TypeChecking.Primitive |
2 (Data Constructor) | Agda.TypeChecking.Primitive |