Agda-2.3.2: 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.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
lambdaLiftExpr | Agda.Syntax.Abstract
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
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
le | Agda.Termination.CallGraph
leaveTop | Agda.TypeChecking.MetaVars.Occurs
LeftAssoc | Agda.Syntax.Fixity
LeftDisjunct | Agda.Auto.NarrowingSearch
leftDistributive | Agda.Utils.TestHelpers
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
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
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 (Type/Class) | Agda.Syntax.Internal
2 (Data Constructor) | Agda.Syntax.Internal
3 (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
Levels | Agda.TypeChecking.MetaVars
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
lhsAsB | Agda.TypeChecking.Rules.LHS.Problem
LHSCore |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
lhsCore | Agda.Syntax.Abstract
LHSCore' | Agda.Syntax.Abstract
lhsCoreAllPatterns | 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
lhsProblem | Agda.TypeChecking.Rules.LHS.Problem
LHSProj |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
LHSRange | Agda.Syntax.Info
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
lhsToSpine | Agda.Syntax.Abstract
lhsWithExpr | Agda.Syntax.Concrete
lhsWithPats | Agda.Syntax.Abstract
lhsWithPattern | Agda.Syntax.Concrete
Lift | Agda.TypeChecking.Substitute
lift | Agda.Auto.CaseSplit
liftCommandM | Agda.Interaction.InteractionTop
liftCommandMT | Agda.Interaction.InteractionTop
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
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
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.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
localNameSpace | Agda.Syntax.Scope.Base
localScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
localState | Agda.Utils.Monad
localTerminationEnv | Agda.Auto.CaseSplit
localTerminationSidecond | Agda.Auto.CaseSplit
localToAbstract | Agda.Syntax.Translation.ConcreteToAbstract
LocalV | Agda.Syntax.Concrete.Operators.Parser
LocalVars | Agda.Syntax.Scope.Base
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.HashMap
2 (Function) | Agda.Utils.Graph
3 (Function) | Agda.Compiler.JS.Substitution
lookupDefault | Agda.Utils.HashMap
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
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
LowerMeta | Agda.Interaction.InteractionTop
lowerMeta | Agda.Interaction.InteractionTop
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