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

Index - L

L 
1 (Data Constructor)Agda.Interaction.EmacsCommand
2 (Data Constructor)Agda.Utils.Map
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
LabelledEdgeAgda.TypeChecking.SizedTypes.WarshallSolver
labelsAgda.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
LambdaAgda.Compiler.JS.Syntax
lambda 
1 (Function)Agda.Compiler.JS.Case
2 (Function)Agda.Syntax.Concrete.Pretty
lambda'Agda.Compiler.JS.Case
LambdaHoleAgda.Syntax.Notation
lambdaLiftExprAgda.Syntax.Abstract
LamBinding 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
LamBinding'Agda.Syntax.Concrete
lamBracketsAgda.Syntax.Fixity
lamFreqAgda.TypeChecking.Test.Generators
LamNotPiAgda.TypeChecking.Rules.Term
LamOrPiAgda.TypeChecking.Rules.Term
LamVAgda.Syntax.Concrete.Operators.Parser
Large 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
largestAgda.TypeChecking.SizedTypes.WarshallSolver
LayoutAgda.Syntax.Parser.Monad
layoutAgda.Syntax.Parser.Lexer
LayoutContextAgda.Syntax.Parser.Monad
layoutKeywordsAgda.Syntax.Parser.Tokens
LazyAgda.Compiler.Epic.AuxAST
lazyAgda.Compiler.Epic.AuxAST
lblBindingsAgda.TypeChecking.Coverage.SplitTree
lblConstructorNameAgda.TypeChecking.Coverage.SplitTree
lblSplitArgAgda.TypeChecking.Coverage.SplitTree
lbraceAgda.Utils.Pretty
lbrackAgda.Utils.Pretty
LCharAgda.Compiler.Epic.AuxAST
lcmpAgda.TypeChecking.SizedTypes.WarshallSolver
LeAgda.TypeChecking.SizedTypes.Syntax
leAgda.Termination.Order
LeastAgda.TypeChecking.SizedTypes.Syntax
leaveTopAgda.TypeChecking.MetaVars.Occurs
LeftAssocAgda.Syntax.Fixity
LeftDisjunctAgda.Auto.NarrowingSearch
leftDistributiveAgda.Utils.TestHelpers
leftExprAgda.TypeChecking.SizedTypes.Syntax
LeftHandSideAgda.Syntax.Translation.ConcreteToAbstract
leftHHAgda.TypeChecking.Rules.LHS.Unify
LeftModeAgda.Utils.Pretty
LeftOfArrowAgda.TypeChecking.Positivity
LeftOperandCtxAgda.Syntax.Fixity
LegendMatrix 
1 (Type/Class)Agda.Utils.Warshall
2 (Data Constructor)Agda.Utils.Warshall
LensCommandLineOptionsAgda.Interaction.Options.Lenses
LensConNameAgda.Syntax.Internal
LensHidingAgda.Syntax.Common
LensIncludeDirsAgda.Interaction.Options.Lenses
LensPersistentVerbosityAgda.Interaction.Options.Lenses
LensPragmaOptionsAgda.Interaction.Options.Lenses
LensRelevanceAgda.Syntax.Common
LensSafeModeAgda.Interaction.Options.Lenses
LensVerbosityAgda.Interaction.Options.Lenses
LeqAgda.TypeChecking.SizedTypes
leqLevelAgda.TypeChecking.Conversion
leqSortAgda.TypeChecking.Conversion
leqTypeAgda.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
LetApplyAgda.Syntax.Abstract
LetBindAgda.Syntax.Abstract
LetBindingAgda.Syntax.Abstract
LetBindingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
LetDefAgda.Syntax.Translation.ConcreteToAbstract
LetDefsAgda.Syntax.Translation.ConcreteToAbstract
LetInfoAgda.Syntax.Info
LetOpenAgda.Syntax.Abstract
LetPatBindAgda.Syntax.Abstract
LetRangeAgda.Syntax.Info
lettAgda.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
LevelAtomAgda.Syntax.Internal
LevelCmpAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
LevelKit 
1 (Type/Class)Agda.TypeChecking.Level
2 (Data Constructor)Agda.TypeChecking.Level
levelLubAgda.TypeChecking.Level
levelMaxAgda.TypeChecking.Substitute
LevelsAgda.TypeChecking.MetaVars
levelSortAgda.TypeChecking.Substitute
levelSucAgda.Syntax.Internal
levelSucFunctionAgda.TypeChecking.Level
levelTmAgda.TypeChecking.Substitute
levelTypeAgda.TypeChecking.Level
levelViewAgda.TypeChecking.Level
levelView'Agda.TypeChecking.Level
LexActionAgda.Syntax.Parser.Alex
lexerAgda.Syntax.Parser.Lexer
lexErrorAgda.Syntax.Parser.Monad, Agda.Syntax.Parser.LexActions
lexInputAgda.Syntax.Parser.Alex
lexPosAgda.Syntax.Parser.Alex
LexPredicateAgda.Syntax.Parser.Alex
lexPrevCharAgda.Syntax.Parser.Alex
LexStateAgda.Syntax.Parser.Monad
lexTokenAgda.Syntax.Parser.LexActions
LFloatAgda.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
lhsAsBAgda.TypeChecking.Rules.LHS.Problem
LHSCore 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
lhsCoreAgda.Syntax.Abstract
LHSCore'Agda.Syntax.Abstract
lhsCoreAddSpineAgda.Syntax.Abstract
lhsCoreAllPatternsAgda.Syntax.Abstract
lhsCoreAppAgda.Syntax.Abstract
lhsCoreToPatternAgda.Syntax.Abstract
lhsCoreToSpineAgda.Syntax.Abstract
lhsDefName 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsDestructor 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
lhsDPIAgda.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
LHSInfoAgda.Syntax.Info
lhsInfoAgda.Syntax.Abstract
lhsOriginalPatternAgda.Syntax.Concrete
LHSOrPatSynAgda.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
lhsProblemAgda.TypeChecking.Rules.LHS.Problem
LHSProj 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
LHSRangeAgda.Syntax.Info
lhsRewriteEqnAgda.Syntax.Concrete
LHSState 
1 (Type/Class)Agda.TypeChecking.Rules.LHS.Problem
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Problem
lhsSubstAgda.TypeChecking.Rules.LHS.Problem
LHSToSpineAgda.Syntax.Abstract
lhsToSpineAgda.Syntax.Abstract
lhsWithExprAgda.Syntax.Concrete
lhsWithPatsAgda.Syntax.Abstract
lhsWithPatternAgda.Syntax.Concrete
LiftAgda.TypeChecking.Substitute
liftAgda.Auto.CaseSplit
liftCommandMTAgda.Interaction.InteractionTop
liftMAgda.Utils.Monad
liftM2Agda.Utils.Monad
liftM3Agda.Utils.Monad
liftM4Agda.Utils.Monad
liftM5Agda.Utils.Monad
liftP 
1 (Function)Agda.Utils.Permutation
2 (Function)Agda.Syntax.Parser.LookAhead
liftSAgda.TypeChecking.Substitute
liftTCMAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
liftUnderAbsAgda.TypeChecking.MetaVars.Occurs
lineLengthAgda.Utils.Pretty
LInfAgda.TypeChecking.SizedTypes.WarshallSolver
LIntAgda.Compiler.Epic.AuxAST
LispAgda.Interaction.EmacsCommand
lispifyHighlightingInfoAgda.Interaction.Highlighting.Emacs
listAgda.TypeChecking.Primitive
List2 
1 (Type/Class)Agda.Utils.Tuple
2 (Data Constructor)Agda.Utils.Tuple
list2Agda.Utils.Tuple
listenDirtyAgda.Utils.Update
ListenerAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
listenToMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
listOfAgda.Utils.QuickCheck
listOf1Agda.Utils.QuickCheck
listOfElementsAgda.Utils.TestHelpers
ListTelAgda.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
litBranchesAgda.TypeChecking.CompiledClause
litCaseAgda.TypeChecking.CompiledClause
LitCharAgda.Syntax.Literal
litCharAgda.Syntax.Parser.StringLiterals
LitDBPAgda.Termination.Monad
LiteralAgda.Syntax.Literal
literal 
1 (Function)Agda.Syntax.Parser.LexActions
2 (Function)Agda.Compiler.MAlonzo.Compiler
3 (Function)Agda.Compiler.JS.Compiler
literateAgda.Syntax.Parser.Lexer
LitFloatAgda.Syntax.Literal
LitFocusAgda.TypeChecking.Rules.LHS.Problem
litFreqAgda.TypeChecking.Test.Generators
LitIntAgda.Syntax.Literal
litIntAgda.Compiler.Epic.Injection
LitMPAgda.TypeChecking.Coverage.Match
LitP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
3 (Data Constructor)Agda.Syntax.Internal
LitQNameAgda.Syntax.Literal
litqnameAgda.Compiler.MAlonzo.Compiler
LitShAgda.TypeChecking.Rules.LHS.Unify
LitStringAgda.Syntax.Literal
litStringAgda.Syntax.Parser.StringLiterals
litToConAgda.Compiler.Epic.Injection
litTypeAgda.TypeChecking.Monad.Builtin
loadFileAgda.Interaction.CommandLine.CommandLine
LocalAgda.Compiler.JS.Syntax
LocalId 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
localidAgda.Compiler.JS.Parser
localNameSpaceAgda.Syntax.Scope.Base
localScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
localStateAgda.Utils.Monad
localTCStateAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
localTerminationEnvAgda.Auto.CaseSplit
localTerminationSidecondAgda.Auto.CaseSplit
localToAbstractAgda.Syntax.Translation.ConcreteToAbstract
LocalVAgda.Syntax.Concrete.Operators.Parser
LocalVarsAgda.Syntax.Scope.Base
LocalVsImportedModuleClashAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
loffsetAgda.TypeChecking.SizedTypes.WarshallSolver
lookAgda.Utils.ReadP
LookAheadAgda.Syntax.Parser.LookAhead
lookInterfaceAgda.Compiler.Epic.CompileState
LookupAgda.Compiler.JS.Syntax
lookup 
1 (Function)Agda.Utils.HashMap
2 (Function)Agda.Utils.BiMap
3 (Function)Agda.Utils.Graph.AdjacencyMap
4 (Function)Agda.Utils.Graph.AdjacencyMap.Unidirectional
5 (Function)Agda.Compiler.JS.Substitution
lookupBVAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
lookupDefaultAgda.Utils.HashMap
lookupDefinitionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
lookupEdge 
1 (Function)Agda.Utils.Warshall
2 (Function)Agda.TypeChecking.SizedTypes.WarshallSolver
lookupInteractionIdAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
lookupInteractionPointAgda.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
lookupMutualBlockAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
lookupPathAgda.Utils.Trie
lookupPatternSynAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
lookupPrimitiveFunctionAgda.TypeChecking.Primitive
lookupPrimitiveFunctionQAgda.TypeChecking.Primitive
lookupSAgda.TypeChecking.Substitute
lookupSectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
lowerBoundsAgda.TypeChecking.SizedTypes.WarshallSolver
lowerMetaAgda.Interaction.InteractionTop
lowMetaPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
lparenAgda.Utils.Pretty
LStringAgda.Compiler.Epic.AuxAST
LtAgda.TypeChecking.SizedTypes.Syntax
ltAgda.Termination.Order
lubAgda.TypeChecking.SizedTypes.WarshallSolver
lub'Agda.TypeChecking.SizedTypes.WarshallSolver
Lvl 
1 (Type/Class)Agda.TypeChecking.Primitive
2 (Data Constructor)Agda.TypeChecking.Primitive
lvlMaxAgda.TypeChecking.Level
lvlSucAgda.TypeChecking.Level
lvlTypeAgda.TypeChecking.Level
lvlViewAgda.TypeChecking.Substitute
lvlZeroAgda.TypeChecking.Level