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 - E

eatNextChar	Agda.Syntax.Parser.LookAhead
Edge
1 (Type/Class)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Data Constructor)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
3 (Type/Class)	Agda.TypeChecking.Positivity
4 (Data Constructor)	Agda.TypeChecking.Positivity
Edge'	Agda.TypeChecking.SizedTypes.WarshallSolver
edgeFromConstraint	Agda.TypeChecking.SizedTypes.WarshallSolver
edgeIn
1 (Function)	Agda.Utils.Graph.AdjacencyMap
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
edges
1 (Function)	Agda.Utils.Graph.AdjacencyMap
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
3 (Function)	Agda.Utils.Warshall
edgesFrom
1 (Function)	Agda.Utils.Graph.AdjacencyMap
2 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
edgesTo	Agda.Utils.Graph.AdjacencyMap.Unidirectional
edgeToLowerBound	Agda.TypeChecking.SizedTypes.WarshallSolver
edgeToUpperBound	Agda.TypeChecking.SizedTypes.WarshallSolver
EE	Agda.Auto.Syntax
EInterface
1 (Type/Class)	Agda.Compiler.Epic.Interface
2 (Data Constructor)	Agda.Compiler.Epic.Interface
EitherOrBoth	Agda.Utils.Map
El	Agda.Syntax.Internal
el	Agda.TypeChecking.Primitive
elements	Agda.Utils.QuickCheck
elementsUnlessEmpty	Agda.Utils.TestHelpers
elems	Agda.Utils.HashMap
eligibleForProjectionLike	Agda.TypeChecking.ProjectionLike
Elim	Agda.Syntax.Internal
Elim'	Agda.Syntax.Internal
ElimCmp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ElimFreqs
1 (Type/Class)	Agda.TypeChecking.Test.Generators
2 (Data Constructor)	Agda.TypeChecking.Test.Generators
elimFreqs	Agda.TypeChecking.Test.Generators
Elims	Agda.Syntax.Internal
elimView	Agda.TypeChecking.ProjectionLike
Ellipsis	Agda.Syntax.Concrete
Elr	Agda.Auto.Syntax
ElseSh	Agda.TypeChecking.Rules.LHS.Unify
emap	Agda.TypeChecking.Records
embDef	Agda.Syntax.Internal.Defs
EmbPrj	Agda.TypeChecking.Serialise
emp	Agda.Compiler.JS.Substitution
empty
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.Pretty
3 (Function)	Agda.Utils.HashMap
4 (Function)	Agda.Utils.BiMap
5 (Function)	Agda.Utils.Null
6 (Function)	Agda.Utils.Graph.AdjacencyMap
7 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
8 (Function)	Agda.Interaction.Highlighting.Range
9 (Function)	Agda.Utils.Favorites
10 (Function)	Agda.Utils.Trie
11 (Function)	Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
12 (Function)	Agda.Termination.CallMatrix
13 (Function)	Agda.Termination.CallGraph
14 (Function)	Agda.TypeChecking.Pretty
emptyBound	Agda.TypeChecking.SizedTypes.WarshallSolver
emptyBranches	Agda.TypeChecking.CompiledClause
emptyC	Agda.Compiler.Epic.Injection
emptyConstraints	Agda.Utils.Warshall
emptyFunction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
emptyGraphs	Agda.TypeChecking.SizedTypes.WarshallSolver
emptyLayout	Agda.Syntax.Parser.Layout
emptyMetaInfo	Agda.Syntax.Info
emptyNameSpace	Agda.Syntax.Scope.Base
emptyPolarities	Agda.TypeChecking.SizedTypes.Syntax
EmptyS	Agda.TypeChecking.Substitute
emptyScope	Agda.Syntax.Scope.Base
emptyScopeInfo	Agda.Syntax.Scope.Base
emptySignature	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
emptySolution
1 (Function)	Agda.TypeChecking.SizedTypes.Syntax
2 (Function)	Agda.Utils.Warshall
EmptyTel	Agda.Syntax.Internal
emptyUEnv	Agda.TypeChecking.Rules.LHS.Unify
emptyUOutput	Agda.TypeChecking.Rules.LHS.Unify
emptyUState	Agda.TypeChecking.Rules.LHS.Unify
empty_layout	Agda.Syntax.Parser.Lexer
enableDisplayForms	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
enablePhantomTypes	Agda.TypeChecking.Polarity
encode	Agda.TypeChecking.Serialise
encodeFile	Agda.TypeChecking.Serialise
encodeInterface	Agda.TypeChecking.Serialise
encodeModuleName	Agda.Compiler.MAlonzo.Encode
end	Agda.Syntax.Parser.LexActions
endBy	Agda.Utils.ReadP
endBy1	Agda.Utils.ReadP
endos	Agda.Termination.Termination
endWith	Agda.Syntax.Parser.LexActions
end_	Agda.Syntax.Parser.LexActions
enterClosure
1 (Function)	Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad
2 (Function)	Agda.TypeChecking.Reduce.Monad
Env	Agda.Syntax.Translation.AbstractToConcrete
envAbstractMode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envActiveProblems	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAllowDestructiveUpdate	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAllowedReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAnonymousModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAppDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAssignMetas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envCall	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envColors	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envContext	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envCurrentModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envCurrentPath	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envDisplayFormsEnabled	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envEtaContractImplicit	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envExpandLast	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envHighlightingLevel	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envHighlightingMethod	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envHighlightingRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envImportPath	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envInsideDotPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envLetBindings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envModuleNestingLevel	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envMutualBlock	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envPrintDomainFreePi	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envReifyInteractionPoints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envRelevance	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envSimplification	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envSolvingConstraints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eof	Agda.Syntax.Parser.LexActions
Epic	Agda.Interaction.InteractionTop
EpicCode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
epicError	Agda.Compiler.Epic.CompileState
EpicFun	Agda.Compiler.Epic.AuxAST
eqelr	Agda.Auto.CaseSplit
eqGroups	Agda.Compiler.Epic.Injection
eqrcBegin	Agda.Auto.Syntax
eqrcCong	Agda.Auto.Syntax
eqrcEnd	Agda.Auto.Syntax
eqrcId	Agda.Auto.Syntax
eqrcStep	Agda.Auto.Syntax
eqrcSym	Agda.Auto.Syntax
EqReasoningConsts
1 (Type/Class)	Agda.Auto.Syntax
2 (Data Constructor)	Agda.Auto.Syntax
EqReasoningState	Agda.Auto.Syntax
EqRSChain	Agda.Auto.Syntax
EqRSNone	Agda.Auto.Syntax
EqRSPrf1	Agda.Auto.Syntax
EqRSPrf2	Agda.Auto.Syntax
EqRSPrf3	Agda.Auto.Syntax
Equal
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.TypeChecking.Rules.LHS.Unify
equalAtom	Agda.TypeChecking.Conversion
Equality	Agda.TypeChecking.Rules.LHS.Unify
equalLevel	Agda.TypeChecking.Conversion
equals
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
equalSort	Agda.TypeChecking.Conversion
equalTerm	Agda.TypeChecking.Conversion
equalType	Agda.TypeChecking.Conversion
Erasure	Agda.Compiler.Epic.Erasure
erasure	Agda.Compiler.Epic.Erasure
ErasureState
1 (Type/Class)	Agda.Compiler.Epic.Erasure
2 (Data Constructor)	Agda.Compiler.Epic.Erasure
eriEqRState	Agda.Auto.SearchControl
eriInfTypeUnknown	Agda.Auto.SearchControl
eriIotaStep	Agda.Auto.SearchControl
eriIsEliminand	Agda.Auto.SearchControl
eriMain	Agda.Auto.SearchControl
eriPickSubsVar	Agda.Auto.SearchControl
eriUnifs	Agda.Auto.SearchControl
eriUsedVars	Agda.Auto.SearchControl
errInput	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
errMsg	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
Error
1 (Data Constructor)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
errorHighlighting	Agda.Interaction.Highlighting.Generate
errPos	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
errPrevToken	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
escape	Agda.Interaction.Highlighting.Vim
escapeContext	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
escChr	Agda.Compiler.JS.Parser
etaContract	Agda.TypeChecking.EtaContract
etaContractBody	Agda.Auto.Convert
etaContractRecord	Agda.TypeChecking.Records
EtaExpand	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
etaExpand	Agda.Compiler.Epic.Static
etaExpandAtRecordType	Agda.TypeChecking.Records
etaExpandBlocked	Agda.TypeChecking.MetaVars
etaExpandBoundVar	Agda.TypeChecking.Records
etaExpandClause	Agda.TypeChecking.Positivity
etaExpandListeners	Agda.TypeChecking.MetaVars
etaExpandMeta	Agda.TypeChecking.MetaVars
etaExpandMetaSafe	Agda.TypeChecking.MetaVars
etaExpandProjectedVar	Agda.TypeChecking.MetaVars
etaExpandRecord	Agda.TypeChecking.Records
etaExpandRecord_	Agda.TypeChecking.Records
etaInequal	Agda.TypeChecking.Conversion
etaOnce	Agda.TypeChecking.EtaContract
EtaPragma
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
ETel
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
eval	Agda.TypeChecking.SizedTypes.Tests
evalIn	Agda.Interaction.CommandLine.CommandLine
evalInCurrent	Agda.Interaction.BasicOps
evalInMeta	Agda.Interaction.BasicOps
evalTerm	Agda.Interaction.CommandLine.CommandLine
Evaluate	Agda.Compiler.Epic.Static
evaluate	Agda.Compiler.Epic.Static
evaluateCC	Agda.Compiler.Epic.Static
everythingInScope	Agda.Syntax.Scope.Base
exact	Agda.Interaction.InteractionTop
Exception	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ExceptionT
1 (Type/Class)	Agda.TypeChecking.Monad.Exception
2 (Data Constructor)	Agda.TypeChecking.Monad.Exception
exhaustive	Agda.Utils.QuickCheck
ExitCode	Agda.Interaction.CommandLine.CommandLine
Exp
1 (Type/Class)	Agda.Compiler.JS.Syntax
2 (Type/Class)	Agda.Auto.Syntax
exp	Agda.Compiler.JS.Parser
exp0	Agda.Compiler.JS.Parser
exp1	Agda.Compiler.JS.Parser
exp2	Agda.Compiler.JS.Parser
exp2'	Agda.Compiler.JS.Parser
exp3	Agda.Compiler.JS.Parser
exp3'	Agda.Compiler.JS.Parser
expandbind	Agda.Auto.NarrowingSearch
expandCatchAlls	Agda.TypeChecking.CompiledClause.Compile
expandExp	Agda.Auto.Syntax
ExpandHidden	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
expandImplicitPattern	Agda.TypeChecking.Rules.LHS.Implicit
expandImplicitPattern'	Agda.TypeChecking.Rules.LHS.Implicit
ExpandInstanceArguments	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ExpandInstances	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ExpandLast	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
expandLitPattern	Agda.TypeChecking.Patterns.Abstract
expandP	Agda.Utils.Permutation
ExpandPatternSynonyms	Agda.TypeChecking.Patterns.Abstract
expandPatternSynonyms	Agda.TypeChecking.Patterns.Abstract
expandProjectedVars	Agda.TypeChecking.MetaVars
expandWithFunctionCall	Agda.Termination.Inlining
expectFailure	Agda.Utils.QuickCheck
explicitForAll	Agda.Compiler.MAlonzo.Compiler
expName	Agda.Compiler.JS.Syntax
Export
1 (Type/Class)	Agda.Compiler.JS.Syntax
2 (Data Constructor)	Agda.Compiler.JS.Syntax
exportedNamesInScope	Agda.Syntax.Scope.Base
exportHaskell	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
exports
1 (Function)	Agda.Compiler.JS.Syntax
2 (Function)	Agda.Compiler.JS.Pretty
Expr
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
3 (Type/Class)	Agda.Compiler.Epic.AuxAST
ExpRefInfo
1 (Type/Class)	Agda.Auto.SearchControl
2 (Data Constructor)	Agda.Auto.SearchControl
ExprHole	Agda.Syntax.Notation
ExprInfo	Agda.Syntax.Info
ExprLike
1 (Type/Class)	Agda.Syntax.Abstract.Views
2 (Type/Class)	Agda.Syntax.Concrete.Generic
exprParser
1 (Function)	Agda.Syntax.Parser.Parser
2 (Function)	Agda.Syntax.Parser
ExprRange	Agda.Syntax.Info
ExprSource	Agda.Syntax.Info
ExprView	Agda.Syntax.Concrete.Operators.Parser
exprView	Agda.Syntax.Concrete.Operators.Parser
extendConf	Agda.TypeChecking.Test.Generators
ExtendedLam
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
ExtendedLambda
1 (Data Constructor)	Agda.Interaction.Response
2 (Data Constructor)	Agda.Interaction.MakeCase
extendlambdaname	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
extendSolution	Agda.Utils.Warshall
ExtendTel	Agda.Syntax.Internal
extendWithTelConf	Agda.TypeChecking.Test.Generators
extractblkinfos	Agda.Auto.NarrowingSearch
extractNthElement	Agda.Utils.List
extractNthElement'	Agda.Utils.List
extraref	Agda.Auto.SearchControl