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
eActiveProblems	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eAllowDestructiveUpdate	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eAllowedReductions	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eAnonymousModules	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eAppDef	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eAssignMetas	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eatNextChar	Agda.Syntax.Parser.LookAhead
eCall	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eCheckingWhere	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eCompareBlocked	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eContext	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eCurrentModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eCurrentPath	Agda.TypeChecking.Monad.Base, 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.TypeChecking.Monad
editDistance	Agda.Utils.List
editDistanceSpec	Agda.Utils.List
EE	Agda.Auto.Syntax
eExpandLast	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
EHCOpts	Agda.Compiler.UHC.Bridge
eHighlightingLevel	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eHighlightingMethod	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eHighlightingRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eImportPath	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eInsideDotPattern	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eInstanceDepth	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
elems
1 (Function)	Agda.Utils.HashMap
2 (Function)	Agda.Utils.Bag
eLetBindings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
eliminateDeadCode	Agda.TypeChecking.DeadCode
eliminateLiteralPatterns	Agda.Compiler.Treeless.EliminateLiteralPatterns
Elims
1 (Type/Class)	Agda.Syntax.Reflected
2 (Type/Class)	Agda.Syntax.Internal
elimView	Agda.TypeChecking.ProjectionLike
Ellipsis	Agda.Syntax.Concrete
Elr	Agda.Auto.Syntax
emap	Agda.TypeChecking.Records
embDef	Agda.Syntax.Internal.Defs
EmbPrj	Agda.TypeChecking.Serialise.Base, Agda.TypeChecking.Serialise
eModuleNestingLevel	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
emp	Agda.Compiler.JS.Substitution
Empty	Agda.Utils.Empty
empty
1 (Function)	Agda.Utils.VarSet
2 (Function)	Agda.Utils.HashMap
3 (Function)	Agda.Utils.BiMap
4 (Function)	Agda.Utils.Bag
5 (Function)	Agda.Utils.Null, Agda.Utils.Trie
6 (Function)	Agda.Utils.Graph.AdjacencyMap.Unidirectional
7 (Function)	Agda.Interaction.Highlighting.Range
emptyBinds	Agda.Compiler.MAlonzo.Misc
emptyBound	Agda.TypeChecking.SizedTypes.WarshallSolver
emptyC	Agda.Compiler.Epic.Injection
emptyConstraints	Agda.Utils.Warshall
emptyDict	Agda.TypeChecking.Serialise.Base
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
emptyOB	Agda.TypeChecking.Positivity
emptyPolarities	Agda.TypeChecking.SizedTypes.Syntax
EmptyRewritePragma	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
emptySolution	Agda.Utils.Warshall
EmptyTel	Agda.Syntax.Internal
empty_layout	Agda.Syntax.Parser.Lexer
eMutualBlock	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
enableCaching	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
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.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
ensureNoCompiledHaskell	Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
ensureNPatterns	Agda.TypeChecking.CompiledClause.Compile
enterClosure
1 (Function)	Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad
2 (Function)	Agda.TypeChecking.Reduce.Monad
EnterSection	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.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
envCheckingWhere	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envClause	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envCompareBlocked	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
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
envInstanceDepth	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
envPrintMetasBare	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envRange	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
envTerminationCheck	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envUnquoteFlags	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eof	Agda.Syntax.Parser.LexActions
EpicCode	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
epicError	Agda.Compiler.Epic.CompileState
EpicFun	Agda.Compiler.Epic.AuxAST
ePrintDomainFreePi	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eqelr	Agda.Auto.CaseSplit
eqFreeVars	Agda.TypeChecking.Rewriting.NonLinMatch
eqGroups	Agda.Compiler.Epic.Injection
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
eqtLevel	Agda.Syntax.Internal
eqtLhs	Agda.Syntax.Internal
eqtName	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
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
equals
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
equalSort	Agda.TypeChecking.Conversion
equalTerm	Agda.TypeChecking.Conversion
equalTerms	Agda.Compiler.Treeless.Compare
equalType	Agda.TypeChecking.Conversion
eRange	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
erasedArity	Agda.Compiler.MAlonzo.Compiler
eraseTerms	Agda.Compiler.Treeless.Erase
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
eRelevance	Agda.TypeChecking.Monad.Base, 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
Error
1 (Type/Class)	Agda.Utils.Except
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
3 (Data Constructor)	Agda.Auto.NarrowingSearch
errorHighlighting	Agda.Interaction.Highlighting.Generate
ErrorPart	Agda.TypeChecking.Unquote
ErrorWarnings	Agda.Interaction.Imports
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
eSimplification	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eSolvingConstraints	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
etaContract	Agda.TypeChecking.EtaContract
etaContractRecord	Agda.TypeChecking.Records
etaEnabled	Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
EtaEquality	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
etaEqualityToBool	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
etaExpandRecord'_	Agda.TypeChecking.Records
etaExpandRecord_	Agda.TypeChecking.Records
etaInequal	Agda.TypeChecking.Conversion
etaOnce	Agda.TypeChecking.EtaContract
ETel
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
eTerminationCheck	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eUnquoteFlags	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eUnquoteNormalise	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
evalIn	Agda.Interaction.CommandLine
evalInCurrent	Agda.Interaction.BasicOps
evalInMeta	Agda.Interaction.BasicOps
evalTCM	Agda.TypeChecking.Unquote
evalTerm	Agda.Interaction.CommandLine
Evaluate	Agda.Compiler.Epic.Static
evaluate	Agda.Compiler.Epic.Static
evaluateCC	Agda.Compiler.Epic.Static
everyPrefix	Agda.Utils.Trie
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
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
expandExp	Agda.Auto.Syntax
ExpandHidden	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
expandImplicitPattern	Agda.TypeChecking.Rules.LHS.Implicit
expandImplicitPattern'	Agda.TypeChecking.Rules.LHS.Implicit
ExpandLast	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
expandLitPattern	Agda.TypeChecking.Patterns.Abstract
expandModuleAssigns	Agda.TypeChecking.Rules.Term
expandP	Agda.Utils.Permutation
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
ExplicitStayExplicit	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ExplicitToInstance
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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.Compiler.Epic.AuxAST
3 (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
extendSolution	Agda.Utils.Warshall
ExtendTel	Agda.Syntax.Internal
ExtLam	Agda.Syntax.Reflected
ExtLamInfo
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
extLamNumHidden	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
extLamNumNonHid	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
extractblkinfos	Agda.Auto.NarrowingSearch
extraref	Agda.Auto.SearchControl