Agda-2.6.2.2.20221106: A dependently typed functional programming language and proof assistant

Index - E

eAbstractModeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eActiveBackendNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eActiveProblemsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EagerEvaluationAgda.Syntax.Treeless, Agda.Compiler.Backend
eAllowedReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eAnonymousModulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eAppDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eAssignMetasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eatNextCharAgda.Syntax.Parser.LookAhead
eCallAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCallByNeedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCheckingWhereAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCheckpointsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCompareBlockedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eConflComputingOverlapAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eContextAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCoverageCheckAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentCheckpointAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentlyElaboratingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentPathAgda.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
edgeFromConstraintAgda.TypeChecking.SizedTypes.WarshallSolver
edgesAgda.Utils.Graph.AdjacencyMap.Unidirectional
edgesFromAgda.Utils.Graph.AdjacencyMap.Unidirectional
edgesToAgda.Utils.Graph.AdjacencyMap.Unidirectional
edgeToLowerBoundAgda.TypeChecking.SizedTypes.WarshallSolver
edgeToUpperBoundAgda.TypeChecking.SizedTypes.WarshallSolver
eDisplayFormsEnabledAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
editDistanceAgda.Utils.List
editDistanceSpecAgda.Utils.List
EEAgda.Auto.Syntax
eExpandLastAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
efExistsAgda.Interaction.Library.Base
efPathAgda.Interaction.Library.Base
eGeneralizedVarsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eGeneralizeMetasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eHighlightingLevelAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eHighlightingMethodAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eHighlightingRangeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eImportPathAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eInjectivityDepthAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eInsideDotPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eInstanceDepthAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eIsDebugPrintingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Either3Agda.Utils.Three
eitherDecodeAgda.Interaction.JSON
eitherDecode'Agda.Interaction.JSON
eitherDecodeFileStrictAgda.Interaction.JSON
eitherDecodeFileStrict'Agda.Interaction.JSON
eitherDecodeStrictAgda.Interaction.JSON
eitherDecodeStrict'Agda.Interaction.JSON
ElAgda.Syntax.Internal
elAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
el'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
el'sAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
ElaborateGiveAgda.Interaction.InteractionTop
elaborate_giveAgda.Interaction.BasicOps
ElementAgda.Utils.Zipper
elemKindsOfNamesAgda.Syntax.Scope.Base
elems 
1 (Function)Agda.Utils.BoolSet
2 (Function)Agda.Utils.Bag
3 (Function)Agda.Utils.SmallSet
4 (Function)Agda.Utils.BiMap
eLetBindingsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eligibleForProjectionLikeAgda.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
ElimCmpAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eliminateCaseDefaultsAgda.Compiler.Treeless.EliminateDefaults
EliminatedAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical
eliminateDeadCodeAgda.TypeChecking.DeadCode
eliminateLiteralPatternsAgda.Compiler.Treeless.EliminateLiteralPatterns
Elims 
1 (Type/Class)Agda.Syntax.Internal
2 (Type/Class)Agda.Syntax.Reflected
ElimTypeAgda.TypeChecking.Records
elimViewAgda.TypeChecking.ProjectionLike
elimViewActionAgda.TypeChecking.CheckInternal
elInfAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
EllipsisAgda.Syntax.Concrete
EllipsisPAgda.Syntax.Concrete
ellipsisRangeAgda.Syntax.Common
ellipsisWithArgsAgda.Syntax.Common
ElrAgda.Auto.Syntax
elSSetAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
emacsModeInteractorAgda.Main
eMakeCaseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
embDefAgda.Syntax.Internal.Defs
embedWriterAgda.Utils.Monad
EmbPrjAgda.TypeChecking.Serialise, Agda.TypeChecking.Serialise.Base
eModalityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
empAgda.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
EmptyAbstractAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyAbstract_Agda.Interaction.Options.Warnings
emptyBindsAgda.Compiler.MAlonzo.Misc
emptyBoundAgda.TypeChecking.SizedTypes.WarshallSolver
emptyCompKitAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
emptyConstraintsAgda.Utils.Warshall
EmptyConstructorAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyConstructor_Agda.Interaction.Options.Warnings
emptyDictAgda.TypeChecking.Serialise.Base
EmptyFieldAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyField_Agda.Interaction.Options.Warnings
emptyFunctionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
emptyFunctionDataAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EmptyGeneralizeAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyGeneralize_Agda.Interaction.Options.Warnings
emptyGraphsAgda.TypeChecking.SizedTypes.WarshallSolver
emptyIdiomBrktAgda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
EmptyInstanceAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyInstance_Agda.Interaction.Options.Warnings
emptyLayoutAgda.Syntax.Parser.Layout
emptyLibFileAgda.Interaction.Library.Base
EmptyMacroAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyMacro_Agda.Interaction.Options.Warnings
emptyMetaInfoAgda.Syntax.Info
EmptyMutualAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyMutual_Agda.Interaction.Options.Warnings
emptyNameSpaceAgda.Syntax.Scope.Base
emptyPolaritiesAgda.TypeChecking.SizedTypes.Syntax
EmptyPostulateAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyPostulate_Agda.Interaction.Options.Warnings
EmptyPrimitiveAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyPrimitive_Agda.Interaction.Options.Warnings
EmptyPrivateAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyPrivate_Agda.Interaction.Options.Warnings
emptyRecordDirectivesAgda.Syntax.Common
EmptyRewritePragmaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EmptyRewritePragma_Agda.Interaction.Options.Warnings
EmptySAgda.Syntax.Internal, Agda.TypeChecking.Substitute
emptyScopeAgda.Syntax.Scope.Base
emptyScopeInfoAgda.Syntax.Scope.Base
emptySignatureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
emptySolution 
1 (Function)Agda.Utils.Warshall
2 (Function)Agda.TypeChecking.SizedTypes.Syntax
EmptyTelAgda.Syntax.Internal
emptyWarningsAndNonFatalErrorsAgda.TypeChecking.Warnings
EmptyWhereAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EmptyWhere_Agda.Interaction.Options.Warnings
empty_layoutAgda.Syntax.Parser.Lexer
eMutualBlockAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
enableCachingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
enableDisplayFormsAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EncloseAgda.Compiler.JS.Pretty
encloseAgda.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
encodeInterfaceAgda.TypeChecking.Serialise
encodeModuleNameAgda.Compiler.MAlonzo.Encode
encodeStringAgda.Compiler.MAlonzo.Misc
EncodeTCMAgda.Interaction.JSON
encodeTCMAgda.Interaction.JSON
EncodingAgda.Interaction.JSON
EndAgda.Syntax.Common
endAgda.Syntax.Parser.LexActions
endosAgda.Termination.Termination
EndoSubstAgda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
endWithAgda.Syntax.Parser.LexActions
end_Agda.Syntax.Parser.LexActions
ensureConAgda.TypeChecking.Unquote
ensureDefAgda.TypeChecking.Unquote
ensureEmptyTypeAgda.TypeChecking.Empty
ensureNPatternsAgda.TypeChecking.CompiledClause.Compile
enterClosure 
1 (Function)Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Closure
2 (Function)Agda.TypeChecking.Reduce.Monad
EnterSectionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EnvAgda.Syntax.Translation.AbstractToConcrete
envAbstractModeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envActiveBackendNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envActiveProblemsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAllowedReductionsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAnonymousModulesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAppDefAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAssignMetasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCallAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCallByNeedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCheckingWhereAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCheckpointsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envClauseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCompareBlockedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envConflComputingOverlapAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envContextAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCoverageCheckAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentCheckpointAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentlyElaboratingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentPathAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envDisplayFormsEnabledAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envExpandLastAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envGeneralizedVarsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envGeneralizeMetasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envHighlightingLevelAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envHighlightingMethodAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envHighlightingRangeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envImportPathAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envInjectivityDepthAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envInsideDotPatternAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envInstanceDepthAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envIsDebugPrintingAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envLetBindingsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envMakeCaseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envModalityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envMutualBlockAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envPrintDomainFreePiAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envPrintingPatternLambdasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envPrintMetasBareAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envRangeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envReconstructedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envReduceDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSimplificationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSolvingConstraintsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSplitOnStrictAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSyntacticEqualityFuelAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envTerminationCheckAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envUnquoteFlagsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EnvWithOptsAgda.Compiler.JS.Compiler
envWorkingOnTypesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eofAgda.Syntax.Parser.LexActions
ePrintDomainFreePiAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ePrintingPatternLambdasAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ePrintMetasBareAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eqBeginStep2Agda.Auto.SearchControl
eqCongAgda.Auto.SearchControl
eqConstructorFormAgda.TypeChecking.Rules.LHS.Unify.Types
eqCountAgda.TypeChecking.Rules.LHS.Unify.Types
eqEndAgda.Auto.SearchControl
eqFreeVarsAgda.TypeChecking.Rewriting.NonLinMatch
eqLHSAgda.TypeChecking.Rules.LHS.Unify.Types
eqLhsAgda.TypeChecking.Rewriting.NonLinMatch
eqrcBeginAgda.Auto.Syntax
eqrcCongAgda.Auto.Syntax
eqrcEndAgda.Auto.Syntax
eqrcIdAgda.Auto.Syntax
eqrcStepAgda.Auto.Syntax
eqrcSymAgda.Auto.Syntax
EqReasoningConsts 
1 (Type/Class)Agda.Auto.Syntax
2 (Data Constructor)Agda.Auto.Syntax
EqReasoningStateAgda.Auto.Syntax
eqRHSAgda.TypeChecking.Rules.LHS.Unify.Types
eqRhsAgda.TypeChecking.Rewriting.NonLinMatch
EqRSChainAgda.Auto.Syntax
EqRSNoneAgda.Auto.Syntax
EqRSPrf1Agda.Auto.Syntax
EqRSPrf2Agda.Auto.Syntax
EqRSPrf3Agda.Auto.Syntax
eqStepAgda.Auto.SearchControl
eqSymAgda.Auto.SearchControl
eqTelAgda.TypeChecking.Rules.LHS.Unify.Types
eqtLhsAgda.Syntax.Internal
eqtNameAgda.Syntax.Internal
eqtParamsAgda.Syntax.Internal
eqtRhsAgda.Syntax.Internal
eqtSortAgda.Syntax.Internal
eqtTypeAgda.Syntax.Internal
eqTypeAgda.TypeChecking.Rewriting.NonLinMatch
Equal 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.TypeChecking.Rules.LHS.Unify.Types
equalAgda.TypeChecking.Rewriting.NonLinMatch
equalAtomAgda.TypeChecking.Conversion
EqualityAgda.TypeChecking.Rules.LHS.Unify.Types
EqualityTypeAgda.Syntax.Internal
EqualityTypeData 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
EqualityUnviewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
equalityUnviewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
EqualityViewAgda.Syntax.Internal
equalityViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
EqualityViewTypeAgda.Syntax.Internal
equalLevelAgda.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
equalSortAgda.TypeChecking.Conversion
EqualSyAgda.TypeChecking.Abstract
equalSyAgda.TypeChecking.Abstract
equalTermAgda.TypeChecking.Conversion
equalTermOnFaceAgda.TypeChecking.Conversion
equalTermsAgda.Compiler.Treeless.Compare
equalTypeAgda.TypeChecking.Conversion
eQuantityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eqUnLevelAgda.TypeChecking.Rules.LHS.Unify.Types
eRangeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Erased 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
erasedArityAgda.Compiler.MAlonzo.Coerce
ErasedDatatypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
erasedFromQuantityAgda.Syntax.Common
eraseLocalVarsAgda.Compiler.JS.Compiler
eraseSBoolAgda.Utils.TypeLits
eraseTermsAgda.Compiler.Treeless.Erase
eraseUnusedActionAgda.TypeChecking.CheckInternal
eReconstructedAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eReduceDefsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eRelevanceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eriEqRStateAgda.Auto.SearchControl
eriInfTypeUnknownAgda.Auto.SearchControl
eriIotaStepAgda.Auto.SearchControl
eriIsEliminandAgda.Auto.SearchControl
eriMainAgda.Auto.SearchControl
eriPickSubsVarAgda.Auto.SearchControl
eriUnifsAgda.Auto.SearchControl
eriUsedVarsAgda.Auto.SearchControl
errInputAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
errIOErrorAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
errMsgAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
errNotConOfAgda.TypeChecking.Rewriting.NonLinPattern
errNotPathAgda.TypeChecking.Rewriting.NonLinPattern
errNotPiAgda.TypeChecking.Rewriting.NonLinPattern
errNotProjOfAgda.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
errorHighlightingAgda.Interaction.Highlighting.Generate
ErrorPartAgda.TypeChecking.Unquote
errorTypeAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
ErrorWarningAgda.Interaction.Highlighting.Precise
ErrorWarningsAgda.TypeChecking.Warnings
errorWarningsAgda.Interaction.Options.Warnings
errPathAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
errPosAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
errPrevTokenAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
errRangeAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
errSrcFileAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
errValidExtsAgda.Syntax.Parser.Monad, Agda.Syntax.Parser
escapeAgda.Interaction.Highlighting.Vim
escapeContextAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
eSimplificationAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eSolvingConstraintsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eSplitOnStrictAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EtaAgda.Syntax.Concrete
etaBranchAgda.TypeChecking.CompiledClause
etaCaseAgda.TypeChecking.CompiledClause
etaConAgda.TypeChecking.EtaContract
etaContractAgda.TypeChecking.EtaContract
etaContractRecordAgda.TypeChecking.Records
etaEnabledAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EtaEqualityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EtaExpandAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
etaExpandActionAgda.TypeChecking.EtaExpand
etaExpandAtRecordTypeAgda.TypeChecking.Records
etaExpandBlockedAgda.TypeChecking.MetaVars
etaExpandBoundVarAgda.TypeChecking.Records
etaExpandClauseAgda.TypeChecking.Functions
EtaExpandEquationAgda.TypeChecking.Rules.LHS.Unify.Types
etaExpandListenersAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
etaExpandMetaAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
etaExpandMetaSafeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
etaExpandMetaTCMAgda.TypeChecking.MetaVars
etaExpandOnceAgda.TypeChecking.EtaExpand
etaExpandProjectedVarAgda.TypeChecking.MetaVars
etaExpandRecordAgda.TypeChecking.Records
etaExpandRecord'Agda.TypeChecking.Records
etaExpandRecord'_Agda.TypeChecking.Records
etaExpandRecord_Agda.TypeChecking.Records
EtaExpandVarAgda.TypeChecking.Rules.LHS.Unify.Types
etaLamAgda.TypeChecking.EtaContract
etaOnceAgda.TypeChecking.EtaContract
EtaPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
eTerminationCheckAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eUnquoteFlagsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eUnquoteNormaliseAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
evalInCurrentAgda.Interaction.BasicOps
evalInMetaAgda.Interaction.BasicOps
evalTCMAgda.TypeChecking.Unquote
EvaluationStrategyAgda.Syntax.Treeless, Agda.Compiler.Backend
EvenLoneAgda.TypeChecking.ProjectionLike
everyPrefixAgda.Utils.Trie
everythingInScopeAgda.Syntax.Scope.Base
everythingInScopeQualifiedAgda.Syntax.Scope.Base
eWorkingOnTypesAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
exactAgda.Interaction.Base
exactConInductionAgda.Syntax.Scope.Base
exactConNameAgda.Syntax.Scope.Base
ExceptionAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ExceptKindsOfNamesAgda.Syntax.Scope.Base
exceptKindsOfNamesAgda.Syntax.Scope.Base
ExeArgAgda.TypeChecking.Unquote
ExecutablesFile 
1 (Type/Class)Agda.Interaction.Library.Base
2 (Data Constructor)Agda.Interaction.Library.Base
ExeNameAgda.Interaction.Library.Base, Agda.Interaction.Library
exitAgdaWithAgda.Interaction.ExitCode
exitCodeToNatAgda.TypeChecking.Unquote
exitSuccessAgda.Interaction.ExitCode
Exp 
1 (Type/Class)Agda.Utils.Haskell.Syntax
2 (Type/Class)Agda.Compiler.JS.Syntax
3 (Type/Class)Agda.Auto.Syntax
expandAtAgda.TypeChecking.Rules.LHS.Unify.Types
expandbindAgda.Auto.NarrowingSearch
ExpandBothAgda.TypeChecking.Rules.LHS.Problem
expandCatchAllsAgda.TypeChecking.CompiledClause.Compile
ExpandedEllipsis 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
expandEnvironmentVariablesAgda.Utils.Environment
ExpandHiddenAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ExpandLastAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
expandLitPatternAgda.TypeChecking.Patterns.Abstract
ExpandMetasAgda.Auto.Syntax
expandMetasAgda.Auto.Syntax
expandModuleAssignsAgda.TypeChecking.Rules.Term
expandPAgda.Utils.Permutation
expandParametersAgda.TypeChecking.Rules.LHS.Unify.Types
ExpandPatternSynonymsAgda.TypeChecking.Patterns.Abstract
expandPatternSynonymsAgda.TypeChecking.Patterns.Abstract
expandPatternSynonyms'Agda.TypeChecking.Patterns.Abstract
expandProjectedVarsAgda.TypeChecking.MetaVars
expandRecordTypeAgda.TypeChecking.Rules.LHS.Unify.Types
expandRecordVarAgda.TypeChecking.Records
expandRecordVarsRecursivelyAgda.TypeChecking.Records
expandTelescopeVarAgda.TypeChecking.Telescope
expandVarAgda.TypeChecking.Rules.LHS.Unify.Types
expandVarParametersAgda.TypeChecking.Rules.LHS.Unify.Types
expandVarRecordTypeAgda.TypeChecking.Rules.LHS.Unify.Types
explainStepAgda.TypeChecking.Rules.LHS.Unify.LeftInverse
explainWhyInScopeAgda.TypeChecking.Errors, Agda.Interaction.EmacsTop
expNameAgda.Compiler.JS.Syntax
Export 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
exportedNamesInScopeAgda.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
exprFieldAAgda.Syntax.Concrete
ExprHoleAgda.Syntax.Notation
ExprInfoAgda.Syntax.Info
ExprLike 
1 (Type/Class)Agda.Syntax.Concrete.Generic
2 (Type/Class)Agda.Syntax.Abstract.Views
exprNoRangeAgda.Syntax.Info
exprParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser
ExprRangeAgda.Syntax.Info
exprToAttributeAgda.Syntax.Concrete.Attribute
exprToPatternWithHolesAgda.Syntax.Concrete
ExprViewAgda.Syntax.Concrete.Operators.Parser
exprViewAgda.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
expSAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
expTelescopeAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
ExpTypeSigAgda.Utils.Haskell.Syntax
ExtendedLam 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
ExtendedLambdaAgda.Interaction.Response
extendedLambdaNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
extendInferredBlockAgda.Syntax.Concrete.Definitions.Types
extendSolutionAgda.Utils.Warshall
ExtendTelAgda.Syntax.Internal
ExtLamAgda.Syntax.Reflected
extLamAbsurdAgda.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
extLamModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
extLamSysAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
extractblkinfosAgda.Auto.NarrowingSearch
extractParametersAgda.TypeChecking.ReconstructParameters
extractPatternAgda.Syntax.Abstract
extrarefAgda.Auto.SearchControl