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

eAbstractMode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eActiveProblems	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EagerEvaluation	Agda.Syntax.Treeless, Agda.Compiler.Backend
eAllowedReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eAnonymousModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eAppDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eAssignMetas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eatNextChar	Agda.Syntax.Parser.LookAhead
eCall	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCallByNeed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCheckingWhere	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCheckpoints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCompareBlocked	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eContext	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCurrentCheckpoint	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCurrentModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCurrentPath	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
edges	Agda.Utils.Graph.AdjacencyMap.Unidirectional
edgesFrom	Agda.Utils.Graph.AdjacencyMap.Unidirectional
edgesTo	Agda.Utils.Graph.AdjacencyMap.Unidirectional
edgeToLowerBound	Agda.TypeChecking.SizedTypes.WarshallSolver
edgeToUpperBound	Agda.TypeChecking.SizedTypes.WarshallSolver
eDisplayFormsEnabled	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
editDistance	Agda.Utils.List
editDistanceSpec	Agda.Utils.List
EE	Agda.Auto.Syntax
eExpandLast	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eGeneralizedVars	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eGeneralizeMetas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eHighlightingLevel	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eHighlightingMethod	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eHighlightingRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eImportPath	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eInjectivityDepth	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eInsideDotPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eInstanceDepth	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eIsDebugPrinting	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Either3	Agda.Utils.Three
EitherOrBoth	Agda.Utils.Map
El	Agda.Syntax.Internal
el	Agda.TypeChecking.Primitive
el'	Agda.TypeChecking.Primitive
ElaborateGive	Agda.Interaction.InteractionTop
Element	Agda.Utils.Zipper
elemNe	Agda.Utils.NonemptyList
elems
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.Bag
eLetBindings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eligibleForProjectionLike	Agda.TypeChecking.ProjectionLike
Elim
1 (Type/Class)	Agda.Syntax.Reflected
2 (Type/Class)	Agda.Syntax.Internal
Elim'
1 (Type/Class)	Agda.Syntax.Reflected
2 (Type/Class)	Agda.Syntax.Internal
ElimCmp	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eliminateCaseDefaults	Agda.Compiler.Treeless.EliminateDefaults
eliminateDeadCode	Agda.TypeChecking.DeadCode
eliminateLiteralPatterns	Agda.Compiler.Treeless.EliminateLiteralPatterns
Elims
1 (Type/Class)	Agda.Syntax.Reflected
2 (Type/Class)	Agda.Syntax.Internal
ElimType	Agda.TypeChecking.Records
elimView	Agda.TypeChecking.ProjectionLike
elInf	Agda.TypeChecking.Primitive
Ellipsis	Agda.Syntax.Concrete
EllipsisP	Agda.Syntax.Concrete
Elr	Agda.Auto.Syntax
emap	Agda.TypeChecking.Records
embDef	Agda.Syntax.Internal.Defs
EmbPrj	Agda.TypeChecking.Serialise.Base, Agda.TypeChecking.Serialise
eModality	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eModuleNestingLevel	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
emp	Agda.Compiler.JS.Substitution
Empty	Agda.Utils.Empty
empty
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.BiMap
3 (Function)	Agda.Utils.HashMap
4 (Function)	Agda.Utils.Bag
5 (Function)	Agda.Utils.IntSet.Infinite
6 (Function)	Agda.Utils.Null, Agda.Utils.Trie
7 (Function)	Agda.Interaction.Highlighting.Range
8 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
EmptyAbstract	Agda.Syntax.Concrete.Definitions
EmptyAbstract_	Agda.Interaction.Options.Warnings
emptyBinds	Agda.Compiler.MAlonzo.Misc
emptyBound	Agda.TypeChecking.SizedTypes.WarshallSolver
emptyCompKit	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
emptyConstraints	Agda.Utils.Warshall
emptyDict	Agda.TypeChecking.Serialise.Base
emptyFunction	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EmptyGeneralize	Agda.Syntax.Concrete.Definitions
EmptyGeneralize_	Agda.Interaction.Options.Warnings
emptyGraphs	Agda.TypeChecking.SizedTypes.WarshallSolver
EmptyInstance	Agda.Syntax.Concrete.Definitions
EmptyInstance_	Agda.Interaction.Options.Warnings
emptyLayout	Agda.Syntax.Parser.Layout
emptyLibFile	Agda.Interaction.Library.Base
EmptyMacro	Agda.Syntax.Concrete.Definitions
EmptyMacro_	Agda.Interaction.Options.Warnings
emptyMetaInfo	Agda.Syntax.Info
EmptyMutual	Agda.Syntax.Concrete.Definitions
EmptyMutual_	Agda.Interaction.Options.Warnings
emptyNameSpace	Agda.Syntax.Scope.Base
emptyOB	Agda.TypeChecking.Positivity
emptyPolarities	Agda.TypeChecking.SizedTypes.Syntax
EmptyPostulate	Agda.Syntax.Concrete.Definitions
EmptyPostulate_	Agda.Interaction.Options.Warnings
EmptyPrimitive	Agda.Syntax.Concrete.Definitions
EmptyPrimitive_	Agda.Interaction.Options.Warnings
EmptyPrivate	Agda.Syntax.Concrete.Definitions
EmptyPrivate_	Agda.Interaction.Options.Warnings
EmptyRewritePragma	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EmptyRewritePragma_	Agda.Interaction.Options.Warnings
EmptyS	Agda.Syntax.Internal, Agda.TypeChecking.Substitute
emptyScope	Agda.Syntax.Scope.Base
emptyScopeInfo	Agda.Syntax.Scope.Base
emptySignature	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
emptySolution
1 (Function)	Agda.TypeChecking.SizedTypes.Syntax
2 (Function)	Agda.Utils.Warshall
EmptyTel	Agda.Syntax.Internal
empty_layout	Agda.Syntax.Parser.Lexer
eMutualBlock	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
enableCaching	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
enableDisplayForms	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
enablePhantomTypes	Agda.TypeChecking.Polarity
encode	Agda.TypeChecking.Serialise
encodeFile	Agda.TypeChecking.Serialise
encodeInterface	Agda.TypeChecking.Serialise
encodeModuleName	Agda.Compiler.MAlonzo.Encode
End	Agda.Syntax.Common
end	Agda.Syntax.Parser.LexActions
endBy	Agda.Utils.Parser.ReadP
endBy1	Agda.Utils.Parser.ReadP
endos	Agda.Termination.Termination
endWith	Agda.Syntax.Parser.LexActions
end_	Agda.Syntax.Parser.LexActions
ensureCon	Agda.TypeChecking.Unquote
ensureDef	Agda.TypeChecking.Unquote
ensureEmptyType	Agda.TypeChecking.Empty
ensureNPatterns	Agda.TypeChecking.CompiledClause.Compile
enterClosure
1 (Function)	Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)	Agda.TypeChecking.Reduce.Monad
EnterSection	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Env	Agda.Syntax.Translation.AbstractToConcrete
envAbstractMode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envActiveProblems	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envAllowedReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envAnonymousModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envAppDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envAssignMetas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCall	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCallByNeed	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCheckingWhere	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCheckOptionConsistency	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCheckpoints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCompareBlocked	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envContext	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCurrentCheckpoint	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCurrentModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCurrentPath	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envDisplayFormsEnabled	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envExpandLast	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envGeneralizedVars	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envGeneralizeMetas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envHighlightingLevel	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envHighlightingMethod	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envHighlightingRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envImportPath	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envInjectivityDepth	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envInsideDotPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envInstanceDepth	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envIsDebugPrinting	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envLetBindings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envModality	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envModuleNestingLevel	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envMutualBlock	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envPrintDomainFreePi	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envPrintingPatternLambdas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envPrintMetasBare	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envRelevance	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envSimplification	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envSolvingConstraints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envTerminationCheck	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envUnquoteFlags	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envWorkingOnTypes	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eof	Agda.Syntax.Parser.LexActions
ePrintDomainFreePi	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ePrintingPatternLambdas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eqBeginStep2	Agda.Auto.SearchControl
eqCong	Agda.Auto.SearchControl
eqEnd	Agda.Auto.SearchControl
eqFreeVars	Agda.TypeChecking.Rewriting.NonLinMatch
eqLhs	Agda.TypeChecking.Rewriting.NonLinMatch
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
eqRhs	Agda.TypeChecking.Rewriting.NonLinMatch
EqRSChain	Agda.Auto.Syntax
EqRSNone	Agda.Auto.Syntax
EqRSPrf1	Agda.Auto.Syntax
EqRSPrf2	Agda.Auto.Syntax
EqRSPrf3	Agda.Auto.Syntax
eqStep	Agda.Auto.SearchControl
eqSym	Agda.Auto.SearchControl
eqtLhs	Agda.Syntax.Internal
eqtName	Agda.Syntax.Internal
eqtParams	Agda.Syntax.Internal
eqtRhs	Agda.Syntax.Internal
eqtSort	Agda.Syntax.Internal
eqtType	Agda.Syntax.Internal
Equal	Agda.Syntax.Concrete
equal	Agda.TypeChecking.Rewriting.NonLinMatch
equalAtom	Agda.TypeChecking.Conversion
equalHeadConstructors	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EqualityType	Agda.Syntax.Internal
equalityUnview	Agda.TypeChecking.Monad.Builtin
EqualityView	Agda.Syntax.Internal
equalityView	Agda.TypeChecking.Monad.Builtin
equalLevel	Agda.TypeChecking.Conversion
equalLevel'	Agda.TypeChecking.Conversion
EqualP
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
equals
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
equalSort	Agda.TypeChecking.Conversion
equalTerm	Agda.TypeChecking.Conversion
equalTermOnFace	Agda.TypeChecking.Conversion
equalTerms	Agda.Compiler.Treeless.Compare
equalType	Agda.TypeChecking.Conversion
eQuantity	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
erasedArity	Agda.Compiler.MAlonzo.Compiler
ErasedDatatype	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eraseSBool	Agda.Utils.TypeLits
eraseTerms	Agda.Compiler.Treeless.Erase
eraseUnusedAction	Agda.TypeChecking.CheckInternal
eRelevance	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
errIOError	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
errMsg	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
Error
1 (Type/Class)	Agda.Utils.Except
2 (Data Constructor)	Agda.Auto.NarrowingSearch
3 (Data Constructor)	Agda.Interaction.Highlighting.Precise
4 (Data Constructor)	Agda.Interaction.InteractionTop
errorHighlighting	Agda.Interaction.Highlighting.Generate
ErrorNonEmpty	Agda.TypeChecking.Empty
ErrorPart	Agda.TypeChecking.Unquote
ErrorWarnings	Agda.TypeChecking.Warnings
errorWarnings	Agda.Interaction.Options.Warnings
errPath	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
errPos	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
errPrevToken	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
errRange	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
errSrcFile	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
errValidExts	Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
escape	Agda.Interaction.Highlighting.Vim
escapeContext	Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eSimplification	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eSolvingConstraints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
etaBranch	Agda.TypeChecking.CompiledClause
etaCase	Agda.TypeChecking.CompiledClause
etaCon	Agda.TypeChecking.EtaContract
etaContract	Agda.TypeChecking.EtaContract
etaContractRecord	Agda.TypeChecking.Records
etaEnabled	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EtaEquality	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EtaExpand	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
etaExpandAction	Agda.TypeChecking.EtaExpand
etaExpandAtRecordType	Agda.TypeChecking.Records
etaExpandBlocked	Agda.TypeChecking.MetaVars
etaExpandBoundVar	Agda.TypeChecking.Records
etaExpandClause	Agda.TypeChecking.Functions
etaExpandListeners	Agda.TypeChecking.MetaVars
etaExpandMeta	Agda.TypeChecking.MetaVars
etaExpandMetaSafe	Agda.TypeChecking.MetaVars
etaExpandOnce	Agda.TypeChecking.EtaExpand
etaExpandProjectedVar	Agda.TypeChecking.MetaVars
etaExpandRecord	Agda.TypeChecking.Records
etaExpandRecord'	Agda.TypeChecking.Records
etaExpandRecord'_	Agda.TypeChecking.Records
etaExpandRecord_	Agda.TypeChecking.Records
etaInequal	Agda.TypeChecking.Conversion
etaLam	Agda.TypeChecking.EtaContract
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
eTerminationCheck	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eUnquoteFlags	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eUnquoteNormalise	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
evalIn	Agda.Interaction.CommandLine
evalInCurrent	Agda.Interaction.BasicOps
evalInMeta	Agda.Interaction.BasicOps
evalTCM	Agda.TypeChecking.Unquote
evalTerm	Agda.Interaction.CommandLine
EvaluationStrategy	Agda.Syntax.Treeless, Agda.Compiler.Backend
everyPrefix	Agda.Utils.Trie
everythingInScope	Agda.Syntax.Scope.Base
everythingInScopeQualified	Agda.Syntax.Scope.Base
eWorkingOnTypes	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
exact	Agda.Interaction.InteractionTop
Exception	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ExceptT	Agda.Utils.Except
ExitCode	Agda.Interaction.CommandLine
Exp
1 (Type/Class)	Agda.Utils.Haskell.Syntax
2 (Type/Class)	Agda.Compiler.JS.Syntax
3 (Type/Class)	Agda.Auto.Syntax
expandbind	Agda.Auto.NarrowingSearch
ExpandBoth	Agda.TypeChecking.Rules.LHS.Problem
expandCatchAlls	Agda.TypeChecking.CompiledClause.Compile
expandEnvironmentVariables	Agda.Utils.Environment
ExpandHidden	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ExpandLast	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
expandLitPattern	Agda.TypeChecking.Patterns.Abstract
ExpandMetas	Agda.Auto.Syntax
expandMetas	Agda.Auto.Syntax
expandModuleAssigns	Agda.TypeChecking.Rules.Term
expandP	Agda.Utils.Permutation
ExpandPatternSynonyms	Agda.TypeChecking.Patterns.Abstract
expandPatternSynonyms	Agda.TypeChecking.Patterns.Abstract
expandPatternSynonyms'	Agda.TypeChecking.Patterns.Abstract
expandProjectedVars	Agda.TypeChecking.MetaVars
expandRecordVar	Agda.TypeChecking.Records
expandRecordVarsRecursively	Agda.TypeChecking.Records
expandTelescopeVar	Agda.TypeChecking.Telescope
expandWithFunctionCall	Agda.Termination.Inlining
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
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
ExpRefInfo
1 (Type/Class)	Agda.Auto.SearchControl
2 (Data Constructor)	Agda.Auto.SearchControl
exprFieldA	Agda.Syntax.Concrete
ExprHole	Agda.Syntax.Notation
ExprInfo	Agda.Syntax.Info
ExprLike
1 (Type/Class)	Agda.Syntax.Concrete.Generic
2 (Type/Class)	Agda.Syntax.Abstract.Views
exprNoRange	Agda.Syntax.Info
exprParser
1 (Function)	Agda.Syntax.Parser.Parser
2 (Function)	Agda.Syntax.Parser
ExprRange	Agda.Syntax.Info
ExprView	Agda.Syntax.Concrete.Operators.Parser
exprView	Agda.Syntax.Concrete.Operators.Parser
ExprWhere
1 (Type/Class)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Concrete
exprWhereParser
1 (Function)	Agda.Syntax.Parser.Parser
2 (Function)	Agda.Syntax.Parser
ExpTypeSig	Agda.Utils.Haskell.Syntax
ExtendedLam
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
ExtendedLambda	Agda.Interaction.Response
extendedLambdaName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
extendSolution	Agda.Utils.Warshall
ExtendTel	Agda.Syntax.Internal
ExtLam	Agda.Syntax.Reflected
ExtLamInfo
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
extLamModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
extLamSys	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
extractblkinfos	Agda.Auto.NarrowingSearch
extraref	Agda.Auto.SearchControl