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

Index - E

eAbstractModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eActiveBackendNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eActiveProblemsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EagerEvaluationAgda.Syntax.Treeless, Agda.Compiler.Backend
eAllowedReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eAnonymousModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eAppDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eAssignMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eatNextCharAgda.Syntax.Parser.LookAhead
eCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCallByNeedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCheckingWhereAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCheckpointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCompareBlockedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eConflComputingOverlapAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eContextAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCoverageCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCurrentCheckpointAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCurrentlyElaboratingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCurrentModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCurrentPathAgda.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
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.TypeChecking.Monad, Agda.Compiler.Backend
editDistanceAgda.Utils.List
editDistanceSpecAgda.Utils.List
EEAgda.Auto.Syntax
eExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eExpandLastBoolAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
efExistsAgda.Interaction.Library.Base
eFoldLetBindingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
efPathAgda.Interaction.Library.Base
eGeneralizedVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eGeneralizeMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eHardCompileTimeModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eHighlightingLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eHighlightingMethodAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eHighlightingRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eImportPathAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eInjectivityDepthAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eInsideDotPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eInstanceDepthAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eIsDebugPrintingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Either3Agda.Utils.Three
eitherDecodeAgda.Interaction.JSON
eitherDecode'Agda.Interaction.JSON
eitherDecodeFileStrictAgda.Interaction.JSON
eitherDecodeFileStrict'Agda.Interaction.JSON
eitherDecodeStrictAgda.Interaction.JSON
eitherDecodeStrict'Agda.Interaction.JSON
eitherDecodeStrictTextAgda.Interaction.JSON
ElAgda.Syntax.Internal
elAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
el'Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
el'sAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
eliminateCaseDefaultsAgda.Compiler.Treeless.EliminateDefaults
EliminatedAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
eliminateDeadCodeAgda.TypeChecking.DeadCode
eliminateLiteralPatternsAgda.Compiler.Treeless.EliminateLiteralPatterns
eliminateTypeAgda.TypeChecking.Records
eliminateType'Agda.TypeChecking.Records
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.Base, Agda.TypeChecking.Primitive
EllipsisAgda.Syntax.Concrete
EllipsisPAgda.Syntax.Concrete
ellipsisRangeAgda.Syntax.Common
ellipsisWithArgsAgda.Syntax.Common
ElrAgda.Auto.Syntax
elsAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
elSSetAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
emacsModeInteractorAgda.Main
eMakeCaseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
embDefAgda.Syntax.Internal.Defs
embedWriterAgda.Utils.Monad
EmbPrjAgda.TypeChecking.Serialise.Base, Agda.TypeChecking.Serialise
empAgda.Compiler.JS.Substitution
Empty 
1 (Type/Class)Agda.Utils.Empty
2 (Data Constructor)Agda.Compiler.JS.Pretty
3 (Data Constructor)Agda.TypeChecking.Serialise.Base
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.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
emptyFunctionDataAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
EmptyReasonAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
emptyRecordDirectivesAgda.Syntax.Common
EmptyRewritePragmaAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EmptyRewritePragma_Agda.Interaction.Options.Warnings
EmptySAgda.Syntax.Internal, Agda.TypeChecking.Substitute
emptyScopeAgda.Syntax.Scope.Base
emptyScopeInfoAgda.Syntax.Scope.Base
emptySignatureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
emptySolution 
1 (Function)Agda.Utils.Warshall
2 (Function)Agda.TypeChecking.SizedTypes.Syntax
EmptyTelAgda.Syntax.Internal
emptyWarningsAndNonFatalErrorsAgda.TypeChecking.Warnings
EmptyWhereAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EmptyWhere_Agda.Interaction.Options.Warnings
empty_layoutAgda.Syntax.Parser.Lexer
eMutualBlockAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
enableCachingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
enableDisplayFormsAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function)Agda.TypeChecking.Reduce.Monad
EnterSectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EnvAgda.Syntax.Translation.AbstractToConcrete
envAbstractModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envActiveBackendNameAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envActiveProblemsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envAllowedReductionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envAnonymousModulesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envAppDefAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envAssignMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCallAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCallByNeedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCheckingWhereAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCheckpointsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envClauseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCompareBlockedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envConflComputingOverlapAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envContextAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCoverageCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCurrentCheckpointAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCurrentlyElaboratingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCurrentModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCurrentOpaqueIdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCurrentPathAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envDisplayFormsEnabledAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envFoldLetBindingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envGeneralizedVarsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envGeneralizeMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envHardCompileTimeModeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envHighlightingLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envHighlightingMethodAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envHighlightingRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envImportPathAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envInjectivityDepthAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envInsideDotPatternAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envInstanceDepthAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envIsDebugPrintingAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envLetBindingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envMakeCaseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envMutualBlockAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envPrintDomainFreePiAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envPrintingPatternLambdasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envPrintMetasBareAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envQuantityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envReconstructedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envReduceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envSimplificationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envSolvingConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envSplitOnStrictAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envSyntacticEqualityFuelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envTerminationCheckAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envUnquoteFlagsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EnvVarsAgda.Utils.Environment
EnvWithOptsAgda.Compiler.JS.Compiler
envWorkingOnTypesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eofAgda.Syntax.Parser.LexActions
ePrintDomainFreePiAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ePrintingPatternLambdasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ePrintMetasBareAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
equalityUnviewAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EqualityViewAgda.Syntax.Internal
equalityViewAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EqualityViewTypeAgda.Syntax.Internal
equalLevelAgda.TypeChecking.Conversion
EqualP 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
equals 
1 (Function)Agda.Syntax.Common.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.TypeChecking.Monad, Agda.Compiler.Backend
eqUnLevelAgda.TypeChecking.Rules.LHS.Unify.Types
eRangeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Erased 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
erasedArityAgda.Compiler.MAlonzo.Coerce
ErasedDatatypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ErasedDatatypeReasonAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
erasedFromQuantityAgda.Syntax.Common
eraseLocalVarsAgda.Compiler.JS.Compiler
eraseSBoolAgda.Utils.TypeLits
eraseTermsAgda.Compiler.Treeless.Erase
eraseUnusedActionAgda.TypeChecking.CheckInternal
eReconstructedAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eReduceDefsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eReduceDefsPairAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Syntax.Common.Aspect, 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.Cubical, Agda.TypeChecking.Primitive
ErrorWarningAgda.Syntax.Common.Aspect, Agda.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.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eSimplificationAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eSolvingConstraintsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eSplitOnStrictAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EtaAgda.Syntax.Concrete
etaBranchAgda.TypeChecking.CompiledClause
etaCaseAgda.TypeChecking.CompiledClause
etaConAgda.TypeChecking.EtaContract
etaContractAgda.TypeChecking.EtaContract
etaContractRecordAgda.TypeChecking.Records
etaEnabledAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EtaEqualityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EtaExpandAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
etaExpandAtRecordTypeAgda.TypeChecking.Records
etaExpandBlockedAgda.TypeChecking.MetaVars
etaExpandBoundVarAgda.TypeChecking.Records
etaExpandClauseAgda.TypeChecking.Functions
EtaExpandEquationAgda.TypeChecking.Rules.LHS.Unify.Types
etaExpandListenersAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
etaExpandMetaAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
etaExpandMetaSafeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend
etaExpandMetaTCMAgda.TypeChecking.MetaVars
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.TypeChecking.Monad, Agda.Compiler.Backend
eUnquoteFlagsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eUnquoteNormaliseAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
exactAgda.Interaction.Base
exactConInductionAgda.Syntax.Scope.Base
exactConNameAgda.Syntax.Scope.Base
exactSplitWarningsAgda.Interaction.Options.Warnings
ExceptionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ExpandedPunAgda.Syntax.Common
expandEnvironmentVariablesAgda.Utils.Environment
expandEnvVarTelescopeAgda.Utils.Environment
ExpandHiddenAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ExpandLastAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ExpectedBindingForParameterAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
explainStepAgda.TypeChecking.Rules.LHS.Unify.LeftInverse
explainWhyInScopeAgda.TypeChecking.Errors, Agda.Interaction.EmacsTop
explicitToFieldAgda.Interaction.JSON
explicitToFieldOmitAgda.Interaction.JSON
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.Cubical, Agda.TypeChecking.Primitive
expTelescopeAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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.TypeChecking.Monad, Agda.Compiler.Backend
extendInferredBlockAgda.Syntax.Concrete.Definitions.Types
extendSolutionAgda.Utils.Warshall
ExtendTelAgda.Syntax.Internal
ExtLamAgda.Syntax.Reflected
extLamAbsurdAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
extLamModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
extLamSysAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
extractblkinfosAgda.Auto.NarrowingSearch
extractParametersAgda.TypeChecking.ReconstructParameters
extractPatternAgda.Syntax.Abstract
extrarefAgda.Auto.SearchControl