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.Compiler.Backend, Agda.TypeChecking.Monad
eActiveBackendName	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eActiveProblems	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EagerEvaluation	Agda.Syntax.Treeless, Agda.Compiler.Backend
eAllowedReductions	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eAnonymousModules	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eAppDef	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eAssignMetas	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eatNextChar	Agda.Syntax.Parser.LookAhead
eCall	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCallByNeed	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCheckingWhere	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCheckpoints	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCompareBlocked	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eConflComputingOverlap	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eContext	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCoverageCheck	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentCheckpoint	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentlyElaborating	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentModule	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentPath	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
editDistance	Agda.Utils.List
editDistanceSpec	Agda.Utils.List
EE	Agda.Auto.Syntax
eExpandLast	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
efExists	Agda.Interaction.Library.Base
efPath	Agda.Interaction.Library.Base
eGeneralizedVars	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eGeneralizeMetas	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eHighlightingLevel	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eHighlightingMethod	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eHighlightingRange	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eImportPath	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eInjectivityDepth	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eInsideDotPattern	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eInstanceDepth	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eIsDebugPrinting	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Either3	Agda.Utils.Three
eitherDecode	Agda.Interaction.JSON
eitherDecode'	Agda.Interaction.JSON
eitherDecodeFileStrict	Agda.Interaction.JSON
eitherDecodeFileStrict'	Agda.Interaction.JSON
eitherDecodeStrict	Agda.Interaction.JSON
eitherDecodeStrict'	Agda.Interaction.JSON
El	Agda.Syntax.Internal
el	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
el'	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
el's	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
ElaborateGive	Agda.Interaction.InteractionTop
elaborate_give	Agda.Interaction.BasicOps
Element	Agda.Utils.Zipper
elemKindsOfNames	Agda.Syntax.Scope.Base
elems
1 (Function)	Agda.Utils.BoolSet
2 (Function)	Agda.Utils.Bag
3 (Function)	Agda.Utils.SmallSet
4 (Function)	Agda.Utils.BiMap
eLetBindings	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eligibleForProjectionLike	Agda.TypeChecking.ProjectionLike
Elim
1 (Type/Class)	Agda.Syntax.Internal
2 (Type/Class)	Agda.Syntax.Reflected
Elim'
1 (Type/Class)	Agda.Syntax.Internal.Elim, Agda.Syntax.Internal
2 (Type/Class)	Agda.Syntax.Reflected
ElimCmp	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eliminateCaseDefaults	Agda.Compiler.Treeless.EliminateDefaults
Eliminated	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
eliminateDeadCode	Agda.TypeChecking.DeadCode
eliminateLiteralPatterns	Agda.Compiler.Treeless.EliminateLiteralPatterns
Elims
1 (Type/Class)	Agda.Syntax.Internal
2 (Type/Class)	Agda.Syntax.Reflected
ElimType	Agda.TypeChecking.Records
elimView	Agda.TypeChecking.ProjectionLike
elimViewAction	Agda.TypeChecking.CheckInternal
elInf	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
Ellipsis	Agda.Syntax.Concrete
EllipsisP	Agda.Syntax.Concrete
ellipsisRange	Agda.Syntax.Common
ellipsisWithArgs	Agda.Syntax.Common
Elr	Agda.Auto.Syntax
elSSet	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
emacsModeInteractor	Agda.Main
eMakeCase	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
embDef	Agda.Syntax.Internal.Defs
embedWriter	Agda.Utils.Monad
EmbPrj	Agda.TypeChecking.Serialise, Agda.TypeChecking.Serialise.Base
eModality	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
emp	Agda.Compiler.JS.Substitution
Empty
1 (Type/Class)	Agda.Utils.Empty
2 (Data Constructor)	Agda.Compiler.JS.Pretty
empty
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.HashTable
3 (Function)	Agda.Utils.BoolSet
4 (Function)	Agda.Utils.Bag
5 (Function)	Agda.Utils.IntSet.Infinite
6 (Function)	Agda.Utils.Null, Agda.Utils.Trie, Agda.Interaction.Highlighting.Range
7 (Function)	Agda.Utils.SmallSet
8 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
EmptyAbstract	Agda.Syntax.Concrete.Definitions.Errors, 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.Compiler.Backend, Agda.TypeChecking.Monad
emptyConstraints	Agda.Utils.Warshall
EmptyConstructor	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyConstructor_	Agda.Interaction.Options.Warnings
emptyDict	Agda.TypeChecking.Serialise.Base
EmptyField	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyField_	Agda.Interaction.Options.Warnings
emptyFunction	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
emptyFunctionData	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EmptyGeneralize	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyGeneralize_	Agda.Interaction.Options.Warnings
emptyGraphs	Agda.TypeChecking.SizedTypes.WarshallSolver
emptyIdiomBrkt	Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
EmptyInstance	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyInstance_	Agda.Interaction.Options.Warnings
emptyLayout	Agda.Syntax.Parser.Layout
emptyLibFile	Agda.Interaction.Library.Base
EmptyMacro	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyMacro_	Agda.Interaction.Options.Warnings
emptyMetaInfo	Agda.Syntax.Info
EmptyMutual	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyMutual_	Agda.Interaction.Options.Warnings
emptyNameSpace	Agda.Syntax.Scope.Base
emptyPolarities	Agda.TypeChecking.SizedTypes.Syntax
EmptyPostulate	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyPostulate_	Agda.Interaction.Options.Warnings
EmptyPrimitive	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyPrimitive_	Agda.Interaction.Options.Warnings
EmptyPrivate	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyPrivate_	Agda.Interaction.Options.Warnings
emptyRecordDirectives	Agda.Syntax.Common
EmptyRewritePragma	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
emptySolution
1 (Function)	Agda.Utils.Warshall
2 (Function)	Agda.TypeChecking.SizedTypes.Syntax
EmptyTel	Agda.Syntax.Internal
emptyWarningsAndNonFatalErrors	Agda.TypeChecking.Warnings
EmptyWhere	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EmptyWhere_	Agda.Interaction.Options.Warnings
empty_layout	Agda.Syntax.Parser.Lexer
eMutualBlock	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
enableCaching	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
enableDisplayForms	Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Enclose	Agda.Compiler.JS.Pretty
enclose	Agda.Compiler.JS.Pretty
encode
1 (Function)	Agda.TypeChecking.Serialise
2 (Function)	Agda.Interaction.JSON
encodeFile
1 (Function)	Agda.TypeChecking.Serialise
2 (Function)	Agda.Interaction.JSON
encodeInterface	Agda.TypeChecking.Serialise
encodeModuleName	Agda.Compiler.MAlonzo.Encode
encodeString	Agda.Compiler.MAlonzo.Misc
EncodeTCM	Agda.Interaction.JSON
encodeTCM	Agda.Interaction.JSON
Encoding	Agda.Interaction.JSON
End	Agda.Syntax.Common
end	Agda.Syntax.Parser.LexActions
endos	Agda.Termination.Termination
EndoSubst	Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Closure
2 (Function)	Agda.TypeChecking.Reduce.Monad
EnterSection	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Env	Agda.Syntax.Translation.AbstractToConcrete
envAbstractMode	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envActiveBackendName	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envActiveProblems	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAllowedReductions	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAnonymousModules	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAppDef	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAssignMetas	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCall	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCallByNeed	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCheckingWhere	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCheckpoints	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envClause	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCompareBlocked	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envConflComputingOverlap	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envContext	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCoverageCheck	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentCheckpoint	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentlyElaborating	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentModule	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentPath	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envDisplayFormsEnabled	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envExpandLast	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envGeneralizedVars	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envGeneralizeMetas	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envHighlightingLevel	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envHighlightingMethod	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envHighlightingRange	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envImportPath	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envInjectivityDepth	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envInsideDotPattern	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envInstanceDepth	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envIsDebugPrinting	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envLetBindings	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envMakeCase	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envModality	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envMutualBlock	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envPrintDomainFreePi	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envPrintingPatternLambdas	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envPrintMetasBare	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envRange	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envReconstructed	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envReduceDefs	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSimplification	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSolvingConstraints	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSplitOnStrict	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSyntacticEqualityFuel	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envTerminationCheck	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envUnquoteFlags	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EnvWithOpts	Agda.Compiler.JS.Compiler
envWorkingOnTypes	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eof	Agda.Syntax.Parser.LexActions
ePrintDomainFreePi	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ePrintingPatternLambdas	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ePrintMetasBare	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eqBeginStep2	Agda.Auto.SearchControl
eqCong	Agda.Auto.SearchControl
eqConstructorForm	Agda.TypeChecking.Rules.LHS.Unify.Types
eqCount	Agda.TypeChecking.Rules.LHS.Unify.Types
eqEnd	Agda.Auto.SearchControl
eqFreeVars	Agda.TypeChecking.Rewriting.NonLinMatch
eqLHS	Agda.TypeChecking.Rules.LHS.Unify.Types
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.Rules.LHS.Unify.Types
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
eqTel	Agda.TypeChecking.Rules.LHS.Unify.Types
eqtLhs	Agda.Syntax.Internal
eqtName	Agda.Syntax.Internal
eqtParams	Agda.Syntax.Internal
eqtRhs	Agda.Syntax.Internal
eqtSort	Agda.Syntax.Internal
eqtType	Agda.Syntax.Internal
eqType	Agda.TypeChecking.Rewriting.NonLinMatch
Equal
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.TypeChecking.Rules.LHS.Unify.Types
equal	Agda.TypeChecking.Rewriting.NonLinMatch
equalAtom	Agda.TypeChecking.Conversion
Equality	Agda.TypeChecking.Rules.LHS.Unify.Types
EqualityType	Agda.Syntax.Internal
EqualityTypeData
1 (Type/Class)	Agda.Syntax.Internal
2 (Data Constructor)	Agda.Syntax.Internal
EqualityUnview	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
equalityUnview	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
EqualityView	Agda.Syntax.Internal
equalityView	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
EqualityViewType	Agda.Syntax.Internal
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
EqualSy	Agda.TypeChecking.Abstract
equalSy	Agda.TypeChecking.Abstract
equalTerm	Agda.TypeChecking.Conversion
equalTermOnFace	Agda.TypeChecking.Conversion
equalTerms	Agda.Compiler.Treeless.Compare
equalType	Agda.TypeChecking.Conversion
eQuantity	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eqUnLevel	Agda.TypeChecking.Rules.LHS.Unify.Types
eRange	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Erased
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
erasedArity	Agda.Compiler.MAlonzo.Coerce
ErasedDatatype	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
erasedFromQuantity	Agda.Syntax.Common
eraseLocalVars	Agda.Compiler.JS.Compiler
eraseSBool	Agda.Utils.TypeLits
eraseTerms	Agda.Compiler.Treeless.Erase
eraseUnusedAction	Agda.TypeChecking.CheckInternal
eReconstructed	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eReduceDefs	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eRelevance	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
errNotConOf	Agda.TypeChecking.Rewriting.NonLinPattern
errNotPath	Agda.TypeChecking.Rewriting.NonLinPattern
errNotPi	Agda.TypeChecking.Rewriting.NonLinPattern
errNotProjOf	Agda.TypeChecking.Rewriting.NonLinPattern
Error
1 (Data Constructor)	Agda.Auto.NarrowingSearch
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
3 (Data Constructor)	Agda.Interaction.Base
4 (Type/Class)	Agda.TypeChecking.SizedTypes.Syntax
errorHighlighting	Agda.Interaction.Highlighting.Generate
ErrorPart	Agda.TypeChecking.Unquote
errorType	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
ErrorWarning	Agda.Interaction.Highlighting.Precise
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
eSimplification	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eSolvingConstraints	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eSplitOnStrict	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Eta	Agda.Syntax.Concrete
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.Compiler.Backend, Agda.TypeChecking.Monad
EtaEquality	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EtaExpand	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
etaExpandAction	Agda.TypeChecking.EtaExpand
etaExpandAtRecordType	Agda.TypeChecking.Records
etaExpandBlocked	Agda.TypeChecking.MetaVars
etaExpandBoundVar	Agda.TypeChecking.Records
etaExpandClause	Agda.TypeChecking.Functions
EtaExpandEquation	Agda.TypeChecking.Rules.LHS.Unify.Types
etaExpandListeners	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
etaExpandMeta	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
etaExpandMetaSafe	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
etaExpandMetaTCM	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
EtaExpandVar	Agda.TypeChecking.Rules.LHS.Unify.Types
etaLam	Agda.TypeChecking.EtaContract
etaOnce	Agda.TypeChecking.EtaContract
EtaPragma
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
eTerminationCheck	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eUnquoteFlags	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eUnquoteNormalise	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
evalInCurrent	Agda.Interaction.BasicOps
evalInMeta	Agda.Interaction.BasicOps
evalTCM	Agda.TypeChecking.Unquote
EvaluationStrategy	Agda.Syntax.Treeless, Agda.Compiler.Backend
EvenLone	Agda.TypeChecking.ProjectionLike
everyPrefix	Agda.Utils.Trie
everythingInScope	Agda.Syntax.Scope.Base
everythingInScopeQualified	Agda.Syntax.Scope.Base
eWorkingOnTypes	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
exact	Agda.Interaction.Base
exactConInduction	Agda.Syntax.Scope.Base
exactConName	Agda.Syntax.Scope.Base
Exception	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ExceptKindsOfNames	Agda.Syntax.Scope.Base
exceptKindsOfNames	Agda.Syntax.Scope.Base
ExeArg	Agda.TypeChecking.Unquote
ExecutablesFile
1 (Type/Class)	Agda.Interaction.Library.Base
2 (Data Constructor)	Agda.Interaction.Library.Base
ExeName	Agda.Interaction.Library.Base, Agda.Interaction.Library
exitAgdaWith	Agda.Interaction.ExitCode
exitCodeToNat	Agda.TypeChecking.Unquote
exitSuccess	Agda.Interaction.ExitCode
Exp
1 (Type/Class)	Agda.Utils.Haskell.Syntax
2 (Type/Class)	Agda.Compiler.JS.Syntax
3 (Type/Class)	Agda.Auto.Syntax
expandAt	Agda.TypeChecking.Rules.LHS.Unify.Types
expandbind	Agda.Auto.NarrowingSearch
ExpandBoth	Agda.TypeChecking.Rules.LHS.Problem
expandCatchAlls	Agda.TypeChecking.CompiledClause.Compile
ExpandedEllipsis
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
expandEnvironmentVariables	Agda.Utils.Environment
ExpandHidden	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ExpandLast	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
expandLitPattern	Agda.TypeChecking.Patterns.Abstract
ExpandMetas	Agda.Auto.Syntax
expandMetas	Agda.Auto.Syntax
expandModuleAssigns	Agda.TypeChecking.Rules.Term
expandP	Agda.Utils.Permutation
expandParameters	Agda.TypeChecking.Rules.LHS.Unify.Types
ExpandPatternSynonyms	Agda.TypeChecking.Patterns.Abstract
expandPatternSynonyms	Agda.TypeChecking.Patterns.Abstract
expandPatternSynonyms'	Agda.TypeChecking.Patterns.Abstract
expandProjectedVars	Agda.TypeChecking.MetaVars
expandRecordType	Agda.TypeChecking.Rules.LHS.Unify.Types
expandRecordVar	Agda.TypeChecking.Records
expandRecordVarsRecursively	Agda.TypeChecking.Records
expandTelescopeVar	Agda.TypeChecking.Telescope
expandVar	Agda.TypeChecking.Rules.LHS.Unify.Types
expandVarParameters	Agda.TypeChecking.Rules.LHS.Unify.Types
expandVarRecordType	Agda.TypeChecking.Rules.LHS.Unify.Types
explainStep	Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
explainWhyInScope	Agda.TypeChecking.Errors, Agda.Interaction.EmacsTop
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
exprToAttribute	Agda.Syntax.Concrete.Attribute
exprToPatternWithHoles	Agda.Syntax.Concrete
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
expS	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
expTelescope	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
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.Compiler.Backend, Agda.TypeChecking.Monad
extendInferredBlock	Agda.Syntax.Concrete.Definitions.Types
extendSolution	Agda.Utils.Warshall
ExtendTel	Agda.Syntax.Internal
ExtLam	Agda.Syntax.Reflected
extLamAbsurd	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ExtLamInfo
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
extLamModule	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
extLamSys	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
extractblkinfos	Agda.Auto.NarrowingSearch
extractParameters	Agda.TypeChecking.ReconstructParameters
extractPattern	Agda.Syntax.Abstract
extraref	Agda.Auto.SearchControl