Index - E
| eAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eActiveBackendName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eActiveProblems | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| EagerEvaluation | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| eAllowedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eAnonymousModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eAppDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eAssignMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eatNextChar | Agda.Syntax.Parser.LookAhead |
| eCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eCallByNeed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eCheckingWhere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eCompareBlocked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eConflComputingOverlap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eCoverageCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eCurrentCheckpoint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eCurrentlyElaborating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eCurrentPath | Agda.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 |
| 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, Agda.Compiler.Backend |
| editDistance | Agda.Utils.List |
| editDistanceSpec | Agda.Utils.List |
| eExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eExpandLastBool | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| efExists | Agda.Interaction.Library.Base |
| eFoldLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| efPath | Agda.Interaction.Library.Base |
| eGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eGeneralizeMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eHardCompileTimeMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eHighlightingLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eHighlightingMethod | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eHighlightingRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eImportPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eInjectivityDepth | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eInsideDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eInstanceDepth | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eIsDebugPrinting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Either3 | Agda.Utils.Three |
| eitherDecode | Agda.Interaction.JSON |
| eitherDecode' | Agda.Interaction.JSON |
| eitherDecodeFileStrict | Agda.Interaction.JSON |
| eitherDecodeFileStrict' | Agda.Interaction.JSON |
| eitherDecodeStrict | Agda.Interaction.JSON |
| eitherDecodeStrict' | Agda.Interaction.JSON |
| eitherDecodeStrictText | Agda.Interaction.JSON |
| El | Agda.Syntax.Internal |
| el | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| el' | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| el's | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| ElaborateGive | Agda.Interaction.InteractionTop |
| elaborate_give | Agda.Interaction.BasicOps |
| elemAt | |
| 1 (Function) | Agda.Utils.Set1 |
| 2 (Function) | Agda.Utils.Map1 |
| Element | Agda.Utils.Zipper |
| elemKindsOfNames | Agda.Syntax.Scope.Base |
| elems | |
| 1 (Function) | Agda.Utils.IArray |
| 2 (Function) | Agda.Utils.Map1 |
| 3 (Function) | Agda.Utils.Set1 |
| 4 (Function) | Agda.Utils.Bag |
| 5 (Function) | Agda.Utils.BoolSet |
| 6 (Function) | Agda.Utils.SmallSet |
| 7 (Function) | Agda.Utils.BiMap |
| eLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eligibleForProjectionLike | Agda.TypeChecking.ProjectionLike |
| Elim | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Type/Class) | Agda.Syntax.Reflected |
| Elim' | |
| 1 (Type/Class) | Agda.Syntax.Internal.Elim, Agda.Syntax.Internal |
| 2 (Type/Class) | Agda.Syntax.Reflected |
| ElimCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eliminateCaseDefaults | Agda.Compiler.Treeless.EliminateDefaults |
| Eliminated | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| eliminateDeadCode | Agda.TypeChecking.DeadCode |
| eliminateLiteralPatterns | Agda.Compiler.Treeless.EliminateLiteralPatterns |
| eliminateType | Agda.TypeChecking.Records |
| eliminateType' | Agda.TypeChecking.Records |
| Elims | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Type/Class) | Agda.Syntax.Reflected |
| ElimType | Agda.TypeChecking.Records |
| elimView | Agda.TypeChecking.ProjectionLike |
| elimViewAction | Agda.TypeChecking.CheckInternal |
| elInf | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| Ellipsis | Agda.Syntax.Concrete |
| EllipsisP | Agda.Syntax.Concrete |
| ellipsisRange | Agda.Syntax.Common |
| ellipsisWithArgs | Agda.Syntax.Common |
| els | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| elSSet | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| emacsLispFiles | Agda.Setup.DataFiles |
| EmacsModeCommand | Agda.Interaction.Options |
| EmacsModeCompile | Agda.Interaction.Options |
| emacsModeDir | Agda.Setup.DataFiles |
| EmacsModeLocate | Agda.Interaction.Options |
| EmacsModeSetup | Agda.Interaction.Options |
| eMakeCase | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| embDef | Agda.Syntax.Internal.Defs |
| embedWriter | Agda.Utils.Monad |
| EmbPrj | Agda.TypeChecking.Serialise.Base, Agda.TypeChecking.Serialise |
| emp | Agda.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.Bag |
| 3 (Function) | Agda.Utils.HashTable |
| 4 (Function) | Agda.Utils.BoolSet |
| 5 (Function) | Agda.Utils.IntSet.Infinite |
| 6 (Function) | Agda.Utils.Null, Agda.Utils.Trie, Agda.Interaction.Highlighting.Range |
| 7 (Function) | Agda.Utils.SmallSet |
| 8 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| EmptyAbstract | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyAbstract_ | Agda.Interaction.Options.Warnings |
| emptyBinds | Agda.Compiler.MAlonzo.Misc |
| emptyBound | Agda.TypeChecking.SizedTypes.WarshallSolver |
| emptyCompKit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| EmptyConstructor | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyConstructor_ | Agda.Interaction.Options.Warnings |
| emptyDict | Agda.TypeChecking.Serialise.Base |
| EmptyDT | Agda.TypeChecking.DiscrimTree.Types |
| EmptyField | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyField_ | Agda.Interaction.Options.Warnings |
| emptyFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| emptyFunctionData | Agda.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 |
| EmptyGeneralize | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyGeneralize_ | Agda.Interaction.Options.Warnings |
| emptyGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| emptyIdiomBrkt | Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty |
| EmptyInstance | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyInstance_ | Agda.Interaction.Options.Warnings |
| emptyLayout | Agda.Syntax.Parser.Layout |
| emptyLibFile | Agda.Interaction.Library.Base |
| EmptyMacro | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyMacro_ | Agda.Interaction.Options.Warnings |
| emptyMetaInfo | Agda.Syntax.Info |
| EmptyMutual | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyMutual_ | Agda.Interaction.Options.Warnings |
| emptyNameSpace | Agda.Syntax.Scope.Base |
| emptyPolarities | Agda.TypeChecking.SizedTypes.Syntax |
| EmptyPolarityPragma | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyPolarityPragma_ | Agda.Interaction.Options.Warnings |
| EmptyPostulate | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyPostulate_ | Agda.Interaction.Options.Warnings |
| EmptyPrimitive | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyPrimitive_ | Agda.Interaction.Options.Warnings |
| EmptyPrivate | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions |
| EmptyPrivate_ | Agda.Interaction.Options.Warnings |
| emptyRecordDirectives | Agda.Syntax.Common |
| EmptyRewritePragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| EmptyRewritePragma_ | Agda.Interaction.Options.Warnings |
| EmptyS | Agda.Syntax.Internal, Agda.TypeChecking.Substitute |
| emptyScope | Agda.Syntax.Scope.Base |
| emptyScopeInfo | Agda.Syntax.Scope.Base |
| emptySignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| emptySolution | Agda.TypeChecking.SizedTypes.Syntax |
| EmptyTel | Agda.Syntax.Internal |
| EmptyTypeOfSizes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| EmptyTypeOfSizes_ | Agda.Interaction.Options.Errors |
| EmptyWhere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| EmptyWhere_ | Agda.Interaction.Options.Warnings |
| empty_layout | Agda.Syntax.Parser.Lexer |
| eMutualBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| enableCaching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| enableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Enclose | Agda.Compiler.JS.Pretty |
| enclose | Agda.Compiler.JS.Pretty |
| encode | |
| 1 (Function) | Agda.Interaction.JSON |
| 2 (Function) | Agda.TypeChecking.Serialise |
| encodeFile | |
| 1 (Function) | Agda.Interaction.JSON |
| 2 (Function) | Agda.TypeChecking.Serialise |
| encodeInterface | Agda.TypeChecking.Serialise |
| encodeModuleName | Agda.Compiler.MAlonzo.Encode |
| encodeString | Agda.Compiler.MAlonzo.Misc |
| EncodeTCM | Agda.Interaction.JSON |
| encodeTCM | Agda.Interaction.JSON |
| Encoding | Agda.Interaction.JSON |
| End | Agda.Syntax.Common |
| end | Agda.Syntax.Parser.LexActions |
| endos | Agda.Termination.Termination |
| EndoSubst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute |
| endWith | Agda.Syntax.Parser.LexActions |
| end_ | Agda.Syntax.Parser.LexActions |
| ensureCon | Agda.TypeChecking.Unquote |
| ensureDef | Agda.TypeChecking.Unquote |
| ensureEmptyType | Agda.TypeChecking.Empty |
| ensureNPatterns | Agda.TypeChecking.CompiledClause.Compile |
| ensureUnqual | Agda.Syntax.Parser.Helpers |
| enterClosure | |
| 1 (Function) | Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Function) | Agda.TypeChecking.Reduce.Monad |
| EnterSection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envActiveBackendName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envActiveProblems | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envAllowedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envAnonymousModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envAppDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envAssignMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCallByNeed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCheckingWhere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCheckpoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCompareBlocked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envConflComputingOverlap | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCoverageCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCurrentCheckpoint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCurrentlyElaborating | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCurrentOpaqueId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envCurrentPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envDisplayFormsEnabled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envFoldLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envGeneralizeMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envHardCompileTimeMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envHighlightingLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envHighlightingMethod | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envHighlightingRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envImportPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envInjectivityDepth | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envInsideDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envInstanceDepth | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envIsDebugPrinting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envMakeCase | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envMutualBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envPrintDomainFreePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envPrintingPatternLambdas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envPrintMetasBare | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envQuantity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envReconstructed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envSimplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envSolvingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envSplitOnStrict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envSyntacticEqualityFuel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envTermCheckReducing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envTerminationCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envUnquoteFlags | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| envUnquoteProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| EnvVars | Agda.Utils.Environment |
| EnvWithOpts | Agda.Compiler.JS.Compiler |
| envWorkingOnTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eof | Agda.Syntax.Parser.LexActions |
| ePrintDomainFreePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ePrintingPatternLambdas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ePrintMetasBare | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eqConstructorForm | Agda.TypeChecking.Rules.LHS.Unify.Types |
| eqCount | Agda.TypeChecking.Rules.LHS.Unify.Types |
| eqFreeVars | Agda.TypeChecking.Rewriting.NonLinMatch |
| eqLHS | Agda.TypeChecking.Rules.LHS.Unify.Types |
| eqLhs | Agda.TypeChecking.Rewriting.NonLinMatch |
| eqRHS | Agda.TypeChecking.Rules.LHS.Unify.Types |
| eqRhs | Agda.TypeChecking.Rewriting.NonLinMatch |
| eqTel | Agda.TypeChecking.Rules.LHS.Unify.Types |
| eqtLhs | Agda.Syntax.Internal |
| eqtName | Agda.Syntax.Internal |
| eqtParams | Agda.Syntax.Internal |
| eqtRhs | Agda.Syntax.Internal |
| eqtSort | Agda.Syntax.Internal |
| eqtType | Agda.Syntax.Internal |
| eqType | Agda.TypeChecking.Rewriting.NonLinMatch |
| Equal | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify.Types |
| equal | Agda.TypeChecking.Rewriting.NonLinMatch |
| equalAtom | Agda.TypeChecking.Conversion |
| Equality | Agda.TypeChecking.Rules.LHS.Unify.Types |
| EqualityType | Agda.Syntax.Internal |
| EqualityTypeData | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| EqualityUnview | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| equalityUnview | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| EqualityView | Agda.Syntax.Internal |
| equalityView | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| EqualityViewType | Agda.Syntax.Internal |
| equalLevel | Agda.TypeChecking.Conversion |
| EqualP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| equals | |
| 1 (Function) | Agda.Syntax.Common.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| equalSort | Agda.TypeChecking.Conversion |
| EqualSy | Agda.TypeChecking.Abstract |
| equalSy | Agda.TypeChecking.Abstract |
| equalTerm | Agda.TypeChecking.Conversion |
| equalTermOnFace | Agda.TypeChecking.Conversion |
| equalTerms | Agda.Compiler.Treeless.Compare |
| equalType | Agda.TypeChecking.Conversion |
| eQuantity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eqUnLevel | Agda.TypeChecking.Rules.LHS.Unify.Types |
| eRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Erased | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| erasedArity | Agda.Compiler.MAlonzo.Coerce |
| ErasedDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ErasedDatatypeReason | Agda.Interaction.Options.Errors, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| erasedDatatypeReasonString | Agda.Interaction.Options.Errors |
| ErasedDatatype_ | Agda.Interaction.Options.Errors |
| erasedFromQuantity | Agda.Syntax.Common |
| eraseSBool | Agda.Utils.TypeLits |
| eraseTerms | Agda.Compiler.Treeless.Erase |
| EraseUnused | Agda.Compiler.ToTreeless |
| eraseUnusedAction | Agda.TypeChecking.CheckInternal |
| eReconstructed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eReduceDefsPair | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| errInput | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| errIOError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| errMsg | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| errNotConOf | Agda.TypeChecking.Rewriting.NonLinPattern |
| errNotPath | Agda.TypeChecking.Rewriting.NonLinPattern |
| errNotPi | Agda.TypeChecking.Rewriting.NonLinPattern |
| errNotProjOf | Agda.TypeChecking.Rewriting.NonLinPattern |
| Error | |
| 1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.Interaction.Base |
| 3 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver |
| errorConflictingAttribute | Agda.Syntax.Parser.Helpers |
| errorConflictingAttributes | Agda.Syntax.Parser.Helpers |
| errorHighlighting | Agda.Interaction.Highlighting.Generate |
| ErrorName | Agda.Interaction.Options.Errors |
| errorNameString | Agda.Interaction.Options.Errors |
| ErrorPart | Agda.TypeChecking.Unquote |
| errorType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| ErrorWarning | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
| ErrorWarnings | Agda.TypeChecking.Warnings |
| errorWarnings | Agda.Interaction.Options.Warnings |
| errPath | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| errPos | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| errPrevToken | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| errRange | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| errSrcFile | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| errValidExts | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
| escape | Agda.Interaction.Highlighting.Vim |
| escapeContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eSimplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eSolvingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eSplitOnStrict | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Eta | Agda.Syntax.Concrete |
| etaBranch | Agda.TypeChecking.CompiledClause |
| etaCase | Agda.TypeChecking.CompiledClause |
| etaCon | Agda.TypeChecking.EtaContract |
| etaContract | Agda.TypeChecking.EtaContract |
| etaContractRecord | Agda.TypeChecking.Records |
| etaEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| EtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| EtaExpand | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| etaExpandAtRecordType | Agda.TypeChecking.Records |
| etaExpandBlocked | Agda.TypeChecking.MetaVars |
| etaExpandBoundVar | Agda.TypeChecking.Records |
| etaExpandClause | Agda.TypeChecking.Functions |
| EtaExpandEquation | Agda.TypeChecking.Rules.LHS.Unify.Types |
| etaExpandListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| etaExpandMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| etaExpandMetaSafe | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| etaExpandMetaTCM | Agda.TypeChecking.MetaVars |
| etaExpandProjectedVar | Agda.TypeChecking.MetaVars |
| etaExpandRecord | Agda.TypeChecking.Records |
| etaExpandRecord' | Agda.TypeChecking.Records |
| etaExpandRecord'_ | Agda.TypeChecking.Records |
| etaExpandRecord_ | Agda.TypeChecking.Records |
| EtaExpandVar | Agda.TypeChecking.Rules.LHS.Unify.Types |
| etaLam | Agda.TypeChecking.EtaContract |
| etaOnce | Agda.TypeChecking.EtaContract |
| EtaPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| eTerminationCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eUnquoteFlags | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| eUnquoteNormalise | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| evalInCurrent | Agda.Interaction.BasicOps |
| evalInMeta | Agda.Interaction.BasicOps |
| evalTCM | Agda.TypeChecking.Unquote |
| EvaluationStrategy | Agda.Syntax.Treeless, Agda.Compiler.Backend |
| EvenLone | Agda.TypeChecking.ProjectionLike |
| everyPrefix | Agda.Utils.Trie |
| everythingInScope | Agda.Syntax.Scope.Base |
| everythingInScopeQualified | Agda.Syntax.Scope.Base |
| eWorkingOnTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| exact | Agda.Interaction.Base |
| exactConInduction | Agda.Syntax.Scope.Base |
| exactConName | Agda.Syntax.Scope.Base |
| exactSplitWarnings | Agda.Interaction.Options.Warnings |
| ExceptKindsOfNames | Agda.Syntax.Scope.Base |
| exceptKindsOfNames | Agda.Syntax.Scope.Base |
| ExeArg | Agda.TypeChecking.Unquote |
| ExecError | |
| 1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| execError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| execErrorName | Agda.TypeChecking.Errors.Names |
| execErrorNameString | Agda.Interaction.Options.Errors |
| ExecError_ | |
| 1 (Type/Class) | Agda.Interaction.Options.Errors |
| 2 (Data Constructor) | Agda.Interaction.Options.Errors |
| ExecutablesFile | |
| 1 (Type/Class) | Agda.Interaction.Library.Base |
| 2 (Data Constructor) | Agda.Interaction.Library.Base |
| ExeMap | Agda.Interaction.Library.Base |
| ExeName | Agda.Interaction.Library.Base, Agda.Interaction.Library |
| ExeNotExecutable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ExeNotExecutable_ | Agda.Interaction.Options.Errors |
| ExeNotFound | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ExeNotFound_ | Agda.Interaction.Options.Errors |
| ExeNotTrusted | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ExeNotTrusted_ | Agda.Interaction.Options.Errors |
| existsM | Agda.Utils.Monad |
| exitAgdaWith | Agda.Interaction.ExitCode |
| exitCodeToNat | Agda.TypeChecking.Unquote |
| exitSuccess | Agda.Interaction.ExitCode |
| Exp | |
| 1 (Type/Class) | Agda.Utils.Haskell.Syntax |
| 2 (Type/Class) | Agda.Compiler.JS.Syntax |
| expandAt | Agda.TypeChecking.Rules.LHS.Unify.Types |
| ExpandBoth | Agda.TypeChecking.Rules.LHS.Problem |
| expandCatchalls | Agda.TypeChecking.CompiledClause.Compile |
| ExpandedEllipsis | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| ExpandedPun | Agda.Syntax.Common |
| expandEnvironmentVariables | Agda.Utils.Environment |
| expandEnvVarTelescope | Agda.Utils.Environment |
| ExpandHidden | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| expandLitPattern | Agda.TypeChecking.Patterns.Abstract |
| expandModuleAssigns | Agda.TypeChecking.Rules.Term |
| expandP | Agda.Utils.Permutation |
| expandParameters | Agda.TypeChecking.Rules.LHS.Unify.Types |
| ExpandPatternSynonyms | Agda.TypeChecking.Patterns.Abstract |
| expandPatternSynonyms | Agda.TypeChecking.Patterns.Abstract |
| expandPatternSynonyms' | Agda.TypeChecking.Patterns.Abstract |
| expandProjectedVars | Agda.TypeChecking.MetaVars |
| expandRecordType | Agda.TypeChecking.Rules.LHS.Unify.Types |
| expandRecordVar | Agda.TypeChecking.Records |
| expandRecordVarsRecursively | Agda.TypeChecking.Records |
| expandTelescopeVar | Agda.TypeChecking.Telescope |
| expandVar | Agda.TypeChecking.Rules.LHS.Unify.Types |
| expandVarParameters | Agda.TypeChecking.Rules.LHS.Unify.Types |
| expandVarRecordType | Agda.TypeChecking.Rules.LHS.Unify.Types |
| ExpectedApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ExpectedApplication_ | Agda.Interaction.Options.Errors |
| ExpectedBindingForParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ExpectedBindingForParameter_ | Agda.Interaction.Options.Errors |
| ExpectedIdentifier | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ExpectedIdentifier_ | Agda.Interaction.Options.Errors |
| ExpectedIntervalLiteral | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ExpectedIntervalLiteral_ | Agda.Interaction.Options.Errors |
| explainStep | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse |
| explainWhyInScope | Agda.TypeChecking.Errors, Agda.Interaction.EmacsTop |
| ExplicitPolarityVsPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ExplicitPolarityVsPragma_ | Agda.Interaction.Options.Errors |
| explicitToField | Agda.Interaction.JSON |
| explicitToFieldOmit | Agda.Interaction.JSON |
| expName | Agda.Compiler.JS.Syntax |
| Export | |
| 1 (Type/Class) | Agda.Compiler.JS.Syntax |
| 2 (Data Constructor) | Agda.Compiler.JS.Syntax |
| exportedNamesInScope | Agda.Syntax.Scope.Base |
| exports | |
| 1 (Function) | Agda.Compiler.JS.Syntax |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| Expr | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| exprAsNameAndPattern | Agda.Syntax.Parser.Helpers |
| exprAsNameOrHiddenNames | Agda.Syntax.Parser.Helpers |
| exprAsNamesAndPatterns | Agda.Syntax.Parser.Helpers |
| exprFieldA | Agda.Syntax.Concrete |
| ExprHole | Agda.Syntax.Notation |
| ExprInfo | Agda.Syntax.Info |
| ExprKind | Agda.Syntax.Common |
| 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 |
| exprToAssignment | Agda.Syntax.Parser.Helpers |
| exprToAttribute | Agda.Syntax.Concrete.Attribute |
| exprToLHS | Agda.Syntax.Parser.Helpers |
| exprToName | Agda.Syntax.Parser.Helpers |
| exprToPattern | Agda.Syntax.Parser.Helpers |
| exprToPatternWithHoles | Agda.Syntax.Concrete |
| ExprView | Agda.Syntax.Concrete.Operators.Parser |
| exprView | Agda.Syntax.Concrete.Operators.Parser |
| ExprWhere | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| exprWhereParser | |
| 1 (Function) | Agda.Syntax.Parser.Parser |
| 2 (Function) | Agda.Syntax.Parser |
| expS | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| expTelescope | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| ExpTypeSig | Agda.Utils.Haskell.Syntax |
| extendContext | Agda.TypeChecking.Rewriting.NonLinMatch |
| ExtendedLam | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| ExtendedLambda | Agda.Interaction.Response.Base, Agda.Interaction.Response |
| extendedLambdaName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| extendInferredBlock | Agda.Syntax.Concrete.Definitions.Types |
| ExtendTel | Agda.Syntax.Internal |
| ExtLam | Agda.Syntax.Reflected |
| extLam | Agda.Syntax.Parser.Helpers |
| extLamAbsurd | Agda.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 |
| extLamModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| extLamSys | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| extlam_dropName | Agda.Interaction.InteractionTop |
| extOrAbsLam | Agda.Syntax.Parser.Helpers |
| extractParameters | Agda.TypeChecking.ReconstructParameters |
| extractPattern | Agda.Syntax.Abstract |