L | |
1 (Data Constructor) | Agda.Utils.Map |
2 (Data Constructor) | Agda.Interaction.EmacsCommand |
Label | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver |
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.WarshallSolver |
label | |
1 (Function) | Agda.Utils.QuickCheck |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
LabelledEdge | Agda.TypeChecking.SizedTypes.WarshallSolver |
LabelPatVars | Agda.Syntax.Internal.Pattern |
labelPatVars | Agda.Syntax.Internal.Pattern |
labels | Agda.Utils.QuickCheck |
Lam | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Data Constructor) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Syntax.Internal |
5 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
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 |
lambdaLiftExpr | Agda.Syntax.Abstract |
LamBinding | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Abstract |
LamBinding' | Agda.Syntax.Concrete |
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 |
Large | |
1 (Data Constructor) | Agda.Utils.QuickCheck |
2 (Type/Class) | Agda.Utils.QuickCheck |
largest | Agda.TypeChecking.SizedTypes.WarshallSolver |
lastMaybe | Agda.Utils.List |
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 |
lazyAbsApp | Agda.TypeChecking.Substitute |
lblBindings | Agda.TypeChecking.Coverage.SplitTree |
lblConstructorName | Agda.TypeChecking.Coverage.SplitTree |
lblSplitArg | Agda.TypeChecking.Coverage.SplitTree |
lbrace | Agda.Utils.Pretty |
lbrack | Agda.Utils.Pretty |
LChar | Agda.Compiler.Epic.AuxAST |
lcmp | Agda.TypeChecking.SizedTypes.WarshallSolver |
Le | Agda.TypeChecking.SizedTypes.Syntax |
le | Agda.Termination.Order |
Least | Agda.TypeChecking.SizedTypes.Syntax |
leaveTop | Agda.TypeChecking.MetaVars.Occurs |
LeftAssoc | Agda.Syntax.Fixity |
LeftDisjunct | Agda.Auto.NarrowingSearch |
leftDistributive | Agda.Utils.TestHelpers |
leftExpr | Agda.TypeChecking.SizedTypes.Syntax |
LeftHandSide | Agda.Syntax.Translation.ConcreteToAbstract |
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 |
Lens' | Agda.Utils.Lens |
lensAccumStatistics | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
lensAccumStatisticsP | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
lensAmodName | Agda.Syntax.Scope.Base |
lensAnameName | Agda.Syntax.Scope.Base |
LensCommandLineOptions | Agda.Interaction.Options.Lenses |
LensConName | Agda.Syntax.Internal |
lensField1 | Agda.Utils.Lens.Examples |
lensField2 | Agda.Utils.Lens.Examples |
LensHiding | Agda.Syntax.Common |
LensIncludeDirs | Agda.Interaction.Options.Lenses |
lensLexInput | Agda.Syntax.Parser.Alex |
lensPersistentState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
LensPersistentVerbosity | Agda.Interaction.Options.Lenses |
LensPragmaOptions | Agda.Interaction.Options.Lenses |
LensRelevance | Agda.Syntax.Common |
LensSafeMode | Agda.Interaction.Options.Lenses |
LensVerbosity | Agda.Interaction.Options.Lenses |
Leq | Agda.TypeChecking.SizedTypes |
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.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
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 |
LetDefs | Agda.Syntax.Translation.ConcreteToAbstract |
LetInfo | Agda.Syntax.Info |
LetOpen | Agda.Syntax.Abstract |
LetPatBind | Agda.Syntax.Abstract |
LetRange | Agda.Syntax.Info |
lett | Agda.Compiler.Epic.AuxAST |
Level | |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
2 (Type/Class) | Agda.Syntax.Internal |
3 (Data Constructor) | Agda.Syntax.Internal |
4 (Type/Class) | Agda.Interaction.Highlighting.Generate |
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 |
LevelReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Levels | Agda.TypeChecking.MetaVars |
levelSort | Agda.TypeChecking.Substitute |
levelSuc | Agda.Syntax.Internal |
levelSucFunction | Agda.TypeChecking.Level |
levelTm | Agda.TypeChecking.Substitute |
levelType | Agda.TypeChecking.Level |
levelView | Agda.TypeChecking.Level |
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 |
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 |
lhsAsB | Agda.TypeChecking.Rules.LHS.Problem |
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 |
lhsCoreAddSpine | Agda.Syntax.Abstract |
lhsCoreAllPatterns | Agda.Syntax.Abstract |
lhsCoreApp | Agda.Syntax.Abstract |
lhsCoreToPattern | Agda.Syntax.Abstract |
lhsCoreToSpine | Agda.Syntax.Abstract |
lhsDefName | |
1 (Function) | Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract |
lhsDestructor | |
1 (Function) | Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract |
lhsDPI | Agda.TypeChecking.Rules.LHS.Problem |
lhsFocus | |
1 (Function) | Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract |
LHSHead | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
LHSInfo | Agda.Syntax.Info |
lhsInfo | Agda.Syntax.Abstract |
lhsOriginalPattern | Agda.Syntax.Concrete |
LHSOrPatSyn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
lhsPats | |
1 (Function) | Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract |
lhsPatsLeft | |
1 (Function) | Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract |
lhsPatsRight | |
1 (Function) | Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract |
lhsPatterns | Agda.TypeChecking.Rules.LHS |
lhsPatternTele | Agda.TypeChecking.Rules.LHS |
lhsPermutation | Agda.TypeChecking.Rules.LHS |
lhsProblem | Agda.TypeChecking.Rules.LHS.Problem |
LHSProj | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
LHSRange | Agda.Syntax.Info |
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 |
lhsSubst | Agda.TypeChecking.Rules.LHS.Problem |
lhsSubstitution | Agda.TypeChecking.Rules.LHS |
LHSToSpine | Agda.Syntax.Abstract |
lhsToSpine | Agda.Syntax.Abstract |
lhsVarNames | Agda.TypeChecking.Rules.LHS |
lhsVarTele | Agda.TypeChecking.Rules.LHS |
lhsWithExpr | Agda.Syntax.Concrete |
lhsWithPats | Agda.Syntax.Abstract |
lhsWithPattern | Agda.Syntax.Concrete |
Lift | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
lift | Agda.Auto.CaseSplit |
liftCommandMT | Agda.Interaction.InteractionTop |
liftM | Agda.Utils.Monad |
liftM2 | Agda.Utils.Monad |
liftM3 | Agda.Utils.Monad |
liftM4 | Agda.Utils.Monad |
liftM5 | Agda.Utils.Monad |
liftP | |
1 (Function) | Agda.Utils.Permutation |
2 (Function) | Agda.Syntax.Parser.LookAhead |
liftS | Agda.TypeChecking.Substitute |
liftTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
liftUnderAbs | Agda.TypeChecking.MetaVars.Occurs |
lineLength | Agda.Utils.Pretty |
LInf | Agda.TypeChecking.SizedTypes.WarshallSolver |
LInt | Agda.Compiler.Epic.AuxAST |
Lisp | Agda.Interaction.EmacsCommand |
lispifyHighlightingInfo | Agda.Interaction.Highlighting.Emacs |
list | Agda.TypeChecking.Primitive |
List2 | |
1 (Type/Class) | Agda.Utils.Tuple |
2 (Data Constructor) | Agda.Utils.Tuple |
list2 | Agda.Utils.Tuple |
listCase | Agda.Utils.List |
listenDirty | Agda.Utils.Update |
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 |
ListTel | Agda.TypeChecking.Substitute |
ListTel' | Agda.TypeChecking.Substitute |
listToMaybe | |
1 (Function) | Agda.Utils.Maybe |
2 (Function) | Agda.Utils.Maybe.Strict |
Lit | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Syntax.Internal |
4 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
5 (Type/Class) | Agda.Compiler.Epic.AuxAST |
litBranches | Agda.TypeChecking.CompiledClause |
litCase | Agda.TypeChecking.CompiledClause |
LitChar | Agda.Syntax.Literal |
litChar | Agda.Syntax.Parser.StringLiterals |
LitDBP | Agda.Termination.Monad |
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 |
litInt | Agda.Compiler.Epic.Injection |
LitMP | Agda.TypeChecking.Coverage.Match |
LitP | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
3 (Data Constructor) | Agda.Syntax.Internal |
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.Monad.Builtin |
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 |
locally | Agda.Utils.Lens |
localNameSpace | Agda.Syntax.Scope.Base |
localScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
localShadowedBy | Agda.Syntax.Scope.Base |
localState | Agda.Utils.Monad |
localTCState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
localTCStateSaving | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
localTerminationEnv | Agda.Auto.CaseSplit |
localTerminationSidecond | Agda.Auto.CaseSplit |
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 |
loffset | Agda.TypeChecking.SizedTypes.WarshallSolver |
LoneProjectionLike | Agda.TypeChecking.ProjectionLike |
look | Agda.Utils.ReadP |
LookAhead | Agda.Syntax.Parser.LookAhead |
lookInterface | Agda.Compiler.Epic.CompileState |
Lookup | Agda.Compiler.JS.Syntax |
lookup | |
1 (Function) | Agda.Utils.HashMap |
2 (Function) | Agda.Utils.BiMap |
3 (Function) | Agda.Utils.Graph.AdjacencyMap |
4 (Function) | Agda.Utils.AssocList |
5 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
6 (Function) | Agda.Compiler.JS.Substitution |
lookupBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
lookupDefault | Agda.Utils.HashMap |
lookupDefinition | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
lookupEdge | |
1 (Function) | Agda.TypeChecking.SizedTypes.WarshallSolver |
2 (Function) | Agda.Utils.Warshall |
lookupInteractionId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
lookupInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
lookupMeta | |
1 (Function) | Agda.Syntax.Internal.Defs |
2 (Function) | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
3 (Function) | Agda.TypeChecking.Reduce.Monad |
lookupMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
lookupPath | Agda.Utils.Trie |
lookupPatternSyn | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
lookupPrimitiveFunction | Agda.TypeChecking.Primitive |
lookupPrimitiveFunctionQ | Agda.TypeChecking.Primitive |
lookupS | Agda.TypeChecking.Substitute |
lookupSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
lowerBounds | Agda.TypeChecking.SizedTypes.WarshallSolver |
lowerMeta | Agda.Interaction.InteractionTop |
lowMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
lparen | Agda.Utils.Pretty |
LString | Agda.Compiler.Epic.AuxAST |
Lt | Agda.TypeChecking.SizedTypes.Syntax |
lt | Agda.Termination.Order |
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 |
lvlView | Agda.TypeChecking.Substitute |
lvlZero | Agda.TypeChecking.Level |