Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- $
- %
- +
- .
- /
- <
- =
- >
- ^
- -
- _
- All

Index - L

L |
1 (Data Constructor) | Agda.Auto.Options
2 (Data Constructor) | Agda.Utils.Map
3 (Data Constructor) | Agda.Interaction.EmacsCommand
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.Auto.Syntax
2 (Data Constructor) | Agda.Syntax.Reflected
3 (Data Constructor) | Agda.Syntax.Concrete
4 (Data Constructor) | Agda.Syntax.Internal
5 (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.Pretty
lambdaAddContext | Agda.TypeChecking.Rules.Term
LambdaBound | Agda.Syntax.Scope.Base
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
lamBindingsToTelescope | Agda.Syntax.Concrete
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
LamV | Agda.Syntax.Concrete.Operators.Parser
LamView |
1 (Type/Class) | Agda.Syntax.Abstract.Views
2 (Data Constructor) | Agda.Syntax.Abstract.Views
lamView | Agda.Syntax.Abstract.Views
lamWhere | Agda.Syntax.Concrete
LanguagePragma | Agda.Utils.Haskell.Syntax
largest | Agda.TypeChecking.SizedTypes.WarshallSolver
last2 | Agda.Utils.List
lastMaybe | Agda.Utils.List
LaTeX | Agda.Interaction.InteractionTop
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
LayoutContext | Agda.Syntax.Parser.Monad
layoutKeywords | Agda.Syntax.Parser.Tokens
Lazy | Agda.Utils.Haskell.Syntax
lazyAbsApp | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
LazyEvaluation | Agda.Syntax.Treeless, Agda.Compiler.Backend
lazyMatch | Agda.TypeChecking.CompiledClause
lblBindings | Agda.TypeChecking.Coverage.SplitTree
lblConstructorName | Agda.TypeChecking.Coverage.SplitTree
lblSplitArg | Agda.TypeChecking.Coverage.SplitTree
lbrace | Agda.Utils.Pretty
lbrack | Agda.Utils.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.Fixity
LeftClosedPOMonoid | Agda.Utils.POMonoid
LeftDisjunct | Agda.Auto.NarrowingSearch
leftExpr | Agda.TypeChecking.SizedTypes.Syntax
LeftHandSide | Agda.Syntax.Translation.ConcreteToAbstract
LeftMode | Agda.Utils.Pretty
LeftOfArrow | Agda.TypeChecking.Positivity.Occurrence
LeftOperandCtx | Agda.Syntax.Fixity
LegendMatrix |
1 (Type/Class) | Agda.Utils.Warshall
2 (Data Constructor) | Agda.Utils.Warshall
LEl | Agda.TypeChecking.Rules.Data
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
LensArgInfo | Agda.Syntax.Common
LensAttribute | Agda.Syntax.Concrete.Attribute
LensCommandLineOptions | Agda.Interaction.Options.Lenses
LensConName | Agda.Syntax.Internal
lensField1 | Agda.Utils.Lens.Examples
lensField2 | Agda.Utils.Lens.Examples
LensFreeVariables | Agda.Syntax.Common
lensFresh | Agda.TypeChecking.Serialise.Base
LensGet | Agda.Utils.Lens
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
lensLexInput | Agda.Syntax.Parser.Alex
LensMap | Agda.Utils.Lens
LensModality | Agda.Syntax.Common
LensNamed | Agda.Syntax.Common
lensNamed | Agda.Syntax.Common
LensOrigin | 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
LensQuantity | Agda.Syntax.Common
LensRelevance | Agda.Syntax.Common
lensReuse | Agda.TypeChecking.Serialise.Base
LensSafeMode | Agda.Interaction.Options.Lenses
LensSet | Agda.Utils.Lens
LensSort | Agda.Syntax.Internal
lensSort | Agda.Syntax.Internal
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 | Agda.Syntax.Abstract
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
LetPatBind | Agda.Syntax.Abstract
LetRange | Agda.Syntax.Info
Level |
1 (Data Constructor) | Agda.Benchmarking, 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, Agda.Compiler.Backend
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, Agda.Compiler.Backend
Levels | Agda.TypeChecking.MetaVars
levelSuc | Agda.Syntax.Internal
levelSucFunction | Agda.TypeChecking.Level
levelSucView | Agda.TypeChecking.Substitute
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
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
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
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
LHSInfo | Agda.Syntax.Info
lhsInfo | Agda.Syntax.Abstract
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
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
libDepends | Agda.Interaction.Library.Base
libFile | Agda.Interaction.Library.Base
libFilePos | Agda.Interaction.Library
libIncludes | Agda.Interaction.Library.Base
LibM | Agda.Interaction.Library
LibName | Agda.Interaction.Library.Base, Agda.Interaction.Library
libName | Agda.Interaction.Library.Base
libNameForCurrentDir | Agda.Interaction.Library.Base
LibPositionInfo |
1 (Type/Class) | Agda.Interaction.Library
2 (Data Constructor) | Agda.Interaction.Library
libraryIncludePaths | Agda.Interaction.Library
LibraryWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
libraryWarningName | Agda.Interaction.Library
libToTCM | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
LibUnknownField_ | Agda.Interaction.Options.Warnings
LibWarning |
1 (Type/Class) | Agda.Interaction.Library
2 (Data Constructor) | Agda.Interaction.Library
LibWarning' | Agda.Interaction.Library.Parse
Lift |
1 (Type/Class) | Agda.Auto.CaseSplit
2 (Data Constructor) | Agda.Syntax.Internal, Agda.TypeChecking.Substitute
lift | Agda.Auto.CaseSplit
lift' | Agda.Auto.CaseSplit
liftCommandMT | Agda.Interaction.InteractionTop
liftCommandMTLocalState | Agda.Interaction.InteractionTop
liftListT | Agda.Utils.ListT
liftLocalState | Agda.Interaction.InteractionTop
liftP |
1 (Function) | Agda.Utils.Permutation
2 (Function) | Agda.Syntax.Parser.LookAhead
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
liftU1 | Agda.TypeChecking.Unquote
liftU2 | Agda.TypeChecking.Unquote
liftUnderAbs | Agda.TypeChecking.MetaVars.Occurs
lIndex | Agda.Utils.IndexedList
lineLength | Agda.Utils.Pretty
LineNumber | Agda.Interaction.Library.Parse
lineNumPos | 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
List2 |
1 (Type/Class) | Agda.Utils.Tuple
2 (Data Constructor) | Agda.Utils.Tuple
list2 | Agda.Utils.Tuple
listCase | Agda.Utils.List
listCaseNe | Agda.Utils.NonemptyList
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.Primitive
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.Reflected
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 |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Type/Class) | Agda.Syntax.Literal
literal |
1 (Function) | Agda.Syntax.Parser.LexActions
2 (Function) | Agda.Compiler.MAlonzo.Compiler
3 (Function) | Agda.Compiler.JS.Compiler
literalsNotImplemented | Agda.Auto.Convert
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
LitNat | Agda.Syntax.Literal
LitP |
1 (Data Constructor) | Agda.Syntax.Reflected
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Internal
4 (Data Constructor) | Agda.Syntax.Abstract
LitQName | Agda.Syntax.Literal
litqname |
1 (Function) | Agda.Compiler.MAlonzo.Compiler
2 (Function) | Agda.Compiler.JS.Compiler
litqnamepat | Agda.Compiler.MAlonzo.Compiler
LitS | Agda.Syntax.Reflected
LitString | Agda.Syntax.Literal
litString |
1 (Function) | Agda.Syntax.Parser.StringLiterals
2 (Function) | Agda.Compiler.MAlonzo.Compiler
litType | Agda.TypeChecking.Monad.Builtin
LitWord64 | Agda.Syntax.Literal
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
loadFile | Agda.Interaction.CommandLine
Local | Agda.Compiler.JS.Syntax
local | Agda.Compiler.JS.Compiler
localBinder | Agda.Syntax.Scope.Base
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
locally | Agda.Utils.Lens
locally' | Agda.Utils.Lens
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
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
LocalTerminationEnv | Agda.Auto.CaseSplit
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, Agda.Compiler.Backend
loffset | Agda.TypeChecking.SizedTypes.WarshallSolver
LoneProjectionLike | Agda.TypeChecking.ProjectionLike
look | Agda.Utils.Parser.ReadP
LookAhead | Agda.Syntax.Parser.LookAhead
lookAheadError | Agda.Syntax.Parser.LookAhead
Lookup | Agda.Compiler.JS.Syntax
lookup |
1 (Function) | Agda.Utils.HashMap
2 (Function) | Agda.Utils.BiMap
3 (Function) | Agda.Utils.Trie
4 (Function) | Agda.Compiler.JS.Substitution
5 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
6 (Function) | Agda.Utils.AssocList
lookupBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupDefault | Agda.Utils.HashMap
lookupDefinition | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupEdge | Agda.TypeChecking.SizedTypes.WarshallSolver
lookupImportedName | Agda.Syntax.Scope.Monad
lookupIndex |
1 (Function) | Agda.Utils.IndexedList
2 (Function) | Agda.Compiler.MAlonzo.Compiler
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
lookupMeta |
1 (Function) | Agda.Syntax.Internal.Defs
2 (Function) | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
3 (Function) | Agda.TypeChecking.Reduce.Monad
lookupMeta' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lookupModuleFromSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
lookupPrimitiveFunctionQ | Agda.TypeChecking.Primitive
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
lowerBounds | Agda.TypeChecking.SizedTypes.WarshallSolver
lowMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
lparen | Agda.Utils.Pretty
lSnd | Agda.Utils.Lens
Lt | Agda.TypeChecking.SizedTypes.Syntax
lt | Agda.Termination.Order
ltrim | Agda.Utils.String
LType |
1 (Data Constructor) | Agda.TypeChecking.Rules.Data
2 (Type/Class) | Agda.TypeChecking.Rules.Data
lTypeLevel | Agda.TypeChecking.Rules.Data
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