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 |
Element | Agda.Utils.Zipper |
elemKindsOfNames | Agda.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 |
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 |
emacsModeInteractor | Agda.Main |
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.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 |
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 |
emptyConstraints | Agda.Utils.Warshall |
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 |
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 | |
1 (Function) | Agda.TypeChecking.SizedTypes.Syntax |
2 (Function) | Agda.Utils.Warshall |
EmptyTel | Agda.Syntax.Internal |
EmptyTypeOfSizes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
emptyWarningsAndNonFatalErrors | Agda.TypeChecking.Warnings |
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.TypeChecking.Serialise |
2 (Function) | Agda.Interaction.JSON |
encodeFile | |
1 (Function) | Agda.TypeChecking.Serialise |
2 (Function) | Agda.Interaction.JSON |
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 |
Env | Agda.Syntax.Translation.AbstractToConcrete |
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 |
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.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
erasedFromQuantity | Agda.Syntax.Common |
eraseLocalVars | Agda.Compiler.JS.Compiler |
eraseSBool | Agda.Utils.TypeLits |
eraseTerms | Agda.Compiler.Treeless.Erase |
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 |
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 |
Exception | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
ExceptKindsOfNames | Agda.Syntax.Scope.Base |
exceptKindsOfNames | Agda.Syntax.Scope.Base |
ExeArg | Agda.TypeChecking.Unquote |
ExecutablesFile | |
1 (Type/Class) | Agda.Interaction.Library.Base |
2 (Data Constructor) | Agda.Interaction.Library.Base |
ExeName | Agda.Interaction.Library.Base, Agda.Interaction.Library |
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 |
ExpectedBindingForParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
explainStep | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse |
explainWhyInScope | Agda.TypeChecking.Errors, Agda.Interaction.EmacsTop |
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 |
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 |
extendSolution | Agda.Utils.Warshall |
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 |