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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

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
eqtRange | 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