Agda-2.6.20240714: 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
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.IArray
2 (Function)Agda.Utils.BoolSet
3 (Function)Agda.Utils.Bag
4 (Function)Agda.Utils.SmallSet
5 (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
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
EmptyDTAgda.TypeChecking.DiscrimTree.Types
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
emptyFunctionData_Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
emptyFunction_Agda.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
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.TypeChecking.SizedTypes.Syntax
2 (Function)Agda.Utils.Warshall
EmptyTelAgda.Syntax.Internal
EmptyTypeOfSizesAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
ensureUnqualAgda.Syntax.Parser.Helpers
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
envUnquoteProblemAgda.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
eqConstructorFormAgda.TypeChecking.Rules.LHS.Unify.Types
eqCountAgda.TypeChecking.Rules.LHS.Unify.Types
eqFreeVarsAgda.TypeChecking.Rewriting.NonLinMatch
eqLHSAgda.TypeChecking.Rules.LHS.Unify.Types
eqLhsAgda.TypeChecking.Rewriting.NonLinMatch
eqRHSAgda.TypeChecking.Rules.LHS.Unify.Types
eqRhsAgda.TypeChecking.Rewriting.NonLinMatch
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
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.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Interaction.Base
3 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
errorConflictingAttributeAgda.Syntax.Parser.Helpers
errorConflictingAttributesAgda.Syntax.Parser.Helpers
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
expandAtAgda.TypeChecking.Rules.LHS.Unify.Types
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
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
exprAsNameAndPatternAgda.Syntax.Parser.Helpers
exprAsNameOrHiddenNamesAgda.Syntax.Parser.Helpers
exprAsNamesAndPatternsAgda.Syntax.Parser.Helpers
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
exprToAssignmentAgda.Syntax.Parser.Helpers
exprToAttributeAgda.Syntax.Concrete.Attribute
exprToLHSAgda.Syntax.Parser.Helpers
exprToNameAgda.Syntax.Parser.Helpers
exprToPatternAgda.Syntax.Parser.Helpers
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
extendContextAgda.TypeChecking.Rewriting.NonLinMatch
ExtendedLam 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
ExtendedLambdaAgda.Interaction.Response.Base, Agda.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
extLamAgda.Syntax.Parser.Helpers
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
extlam_dropNameAgda.Interaction.InteractionTop
extOrAbsLamAgda.Syntax.Parser.Helpers
extractParametersAgda.TypeChecking.ReconstructParameters
extractPatternAgda.Syntax.Abstract