Agda-2.6.2.2: 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.Compiler.Backend, Agda.TypeChecking.Monad
eActiveBackendName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eActiveProblems | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EagerEvaluation | Agda.Syntax.Treeless, Agda.Compiler.Backend
eAllowedReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eAnonymousModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eAppDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eAssignMetas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eatNextChar | Agda.Syntax.Parser.LookAhead
eCall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCallByNeed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCheckingWhere | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCheckpoints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCompareBlocked | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eConflComputingOverlap | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eContext | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCoverageCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentCheckpoint | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentlyElaborating | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eCurrentPath | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
editDistance | Agda.Utils.List
editDistanceSpec | Agda.Utils.List
EE | Agda.Auto.Syntax
eExpandLast | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
efExists | Agda.Interaction.Library.Base
efPath | Agda.Interaction.Library.Base
eGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eGeneralizeMetas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eHighlightingLevel | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eHighlightingMethod | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eHighlightingRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eImportPath | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eInjectivityDepth | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eInsideDotPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eInstanceDepth | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eIsDebugPrinting | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
El | Agda.Syntax.Internal
el | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
el' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
el's | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
ElaborateGive | Agda.Interaction.InteractionTop
elaborate_give | Agda.Interaction.BasicOps
Element | Agda.Utils.Zipper
elemKindsOfNames | Agda.Syntax.Scope.Base
elems |
1 (Function) | Agda.Utils.Bag
2 (Function) | Agda.Utils.SmallSet
3 (Function) | Agda.Utils.BiMap
eLetBindings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
eliminateCaseDefaults | Agda.Compiler.Treeless.EliminateDefaults
Eliminated | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
eliminateDeadCode | Agda.TypeChecking.DeadCode
eliminateLiteralPatterns | Agda.Compiler.Treeless.EliminateLiteralPatterns
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, Agda.TypeChecking.Primitive.Base
Ellipsis | Agda.Syntax.Concrete
EllipsisP | Agda.Syntax.Concrete
ellipsisRange | Agda.Syntax.Common
ellipsisWithArgs | Agda.Syntax.Common
Elr | Agda.Auto.Syntax
elSSet | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
emacsModeInteractor | Agda.Main
eMakeCase | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
embDef | Agda.Syntax.Internal.Defs
EmbPrj | Agda.TypeChecking.Serialise, Agda.TypeChecking.Serialise.Base
eModality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
emp | Agda.Compiler.JS.Substitution
Empty |
1 (Type/Class) | Agda.Utils.Empty
2 (Data Constructor) | Agda.Compiler.JS.Pretty
empty |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.Bag
3 (Function) | Agda.Utils.IntSet.Infinite
4 (Function) | Agda.Utils.Null, Agda.Utils.Trie, Agda.Interaction.Highlighting.Range
5 (Function) | Agda.Utils.SmallSet
6 (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.Compiler.Backend, Agda.TypeChecking.Monad
emptyConstraints | Agda.Utils.Warshall
EmptyConstructor | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyConstructor_ | Agda.Interaction.Options.Warnings
emptyDict | Agda.TypeChecking.Serialise.Base
EmptyField | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
EmptyField_ | Agda.Interaction.Options.Warnings
emptyFunction | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
emptySolution |
1 (Function) | Agda.TypeChecking.SizedTypes.Syntax
2 (Function) | Agda.Utils.Warshall
EmptyTel | Agda.Syntax.Internal
emptyWarningsAndNonFatalErrors | Agda.TypeChecking.Warnings
EmptyWhere | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EmptyWhere_ | Agda.Interaction.Options.Warnings
empty_layout | Agda.Syntax.Parser.Lexer
eMutualBlock | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
enableCaching | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
enableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
enterClosure |
1 (Function) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Closure
2 (Function) | Agda.TypeChecking.Reduce.Monad
EnterSection | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Env | Agda.Syntax.Translation.AbstractToConcrete
envAbstractMode | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envActiveBackendName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envActiveProblems | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAllowedReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAnonymousModules | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAppDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envAssignMetas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCall | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCallByNeed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCheckingWhere | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCheckpoints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envClause | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCompareBlocked | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envConflComputingOverlap | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envContext | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCoverageCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentCheckpoint | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentlyElaborating | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envCurrentPath | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envDisplayFormsEnabled | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envExpandLast | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envGeneralizeMetas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envHighlightingLevel | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envHighlightingMethod | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envHighlightingRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envImportPath | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envInjectivityDepth | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envInsideDotPattern | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envInstanceDepth | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envIsDebugPrinting | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envLetBindings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envMakeCase | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envModality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envMutualBlock | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envPrintDomainFreePi | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envPrintingPatternLambdas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envPrintMetasBare | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envReconstructed | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envReduceDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSimplification | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSolvingConstraints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envSplitOnStrict | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envTerminationCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
envUnquoteFlags | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EnvWithOpts | Agda.Compiler.JS.Compiler
envWorkingOnTypes | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eof | Agda.Syntax.Parser.LexActions
ePrintDomainFreePi | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ePrintingPatternLambdas | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ePrintMetasBare | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eqBeginStep2 | Agda.Auto.SearchControl
eqCong | Agda.Auto.SearchControl
eqEnd | Agda.Auto.SearchControl
eqFreeVars | Agda.TypeChecking.Rewriting.NonLinMatch
eqLhs | Agda.TypeChecking.Rewriting.NonLinMatch
eqrcBegin | Agda.Auto.Syntax
eqrcCong | Agda.Auto.Syntax
eqrcEnd | Agda.Auto.Syntax
eqrcId | Agda.Auto.Syntax
eqrcStep | Agda.Auto.Syntax
eqrcSym | Agda.Auto.Syntax
EqReasoningConsts |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
EqReasoningState | Agda.Auto.Syntax
eqRhs | Agda.TypeChecking.Rewriting.NonLinMatch
EqRSChain | Agda.Auto.Syntax
EqRSNone | Agda.Auto.Syntax
EqRSPrf1 | Agda.Auto.Syntax
EqRSPrf2 | Agda.Auto.Syntax
EqRSPrf3 | Agda.Auto.Syntax
eqStep | Agda.Auto.SearchControl
eqSym | Agda.Auto.SearchControl
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 | Agda.Syntax.Concrete
equal | Agda.TypeChecking.Rewriting.NonLinMatch
equalAtom | Agda.TypeChecking.Conversion
EqualityType | Agda.Syntax.Internal
equalityUnview | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
EqualityView | Agda.Syntax.Internal
equalityView | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
equalLevel | Agda.TypeChecking.Conversion
EqualP |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
equals |
1 (Function) | Agda.Utils.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.Compiler.Backend, Agda.TypeChecking.Monad
eRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Erased |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
erasedArity | Agda.Compiler.MAlonzo.Coerce
ErasedDatatype | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
eReduceDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eRelevance | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eriEqRState | Agda.Auto.SearchControl
eriInfTypeUnknown | Agda.Auto.SearchControl
eriIotaStep | Agda.Auto.SearchControl
eriIsEliminand | Agda.Auto.SearchControl
eriMain | Agda.Auto.SearchControl
eriPickSubsVar | Agda.Auto.SearchControl
eriUnifs | Agda.Auto.SearchControl
eriUsedVars | Agda.Auto.SearchControl
errInput | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
errIOError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
errMsg | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser
Error |
1 (Data Constructor) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
3 (Data Constructor) | Agda.Interaction.Base
errorHighlighting | Agda.Interaction.Highlighting.Generate
ErrorPart | Agda.TypeChecking.Unquote
ErrorWarning | 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
eSimplification | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eSolvingConstraints | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eSplitOnStrict | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
EtaEquality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
EtaExpand | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
etaExpandAction | Agda.TypeChecking.EtaExpand
etaExpandAtRecordType | Agda.TypeChecking.Records
etaExpandBlocked | Agda.TypeChecking.MetaVars
etaExpandBoundVar | Agda.TypeChecking.Records
etaExpandClause | Agda.TypeChecking.Functions
etaExpandListeners | Agda.TypeChecking.MetaVars
etaExpandMeta | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars
etaExpandMetaSafe | Agda.TypeChecking.MetaVars
etaExpandMetaTCM | Agda.TypeChecking.MetaVars
etaExpandOnce | Agda.TypeChecking.EtaExpand
etaExpandProjectedVar | Agda.TypeChecking.MetaVars
etaExpandRecord | Agda.TypeChecking.Records
etaExpandRecord' | Agda.TypeChecking.Records
etaExpandRecord'_ | Agda.TypeChecking.Records
etaExpandRecord_ | Agda.TypeChecking.Records
etaLam | Agda.TypeChecking.EtaContract
etaOnce | Agda.TypeChecking.EtaContract
EtaPragma |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
ETel |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
eTerminationCheck | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eUnquoteFlags | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
eUnquoteNormalise | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
exact | Agda.Interaction.Base
exactConInduction | Agda.Syntax.Scope.Base
exactConName | Agda.Syntax.Scope.Base
Exception | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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
3 (Type/Class) | Agda.Auto.Syntax
expandbind | Agda.Auto.NarrowingSearch
ExpandBoth | Agda.TypeChecking.Rules.LHS.Problem
expandCatchAlls | Agda.TypeChecking.CompiledClause.Compile
ExpandedEllipsis |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
expandEnvironmentVariables | Agda.Utils.Environment
ExpandHidden | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ExpandLast | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
expandLitPattern | Agda.TypeChecking.Patterns.Abstract
ExpandMetas | Agda.Auto.Syntax
expandMetas | Agda.Auto.Syntax
expandModuleAssigns | Agda.TypeChecking.Rules.Term
expandP | Agda.Utils.Permutation
ExpandPatternSynonyms | Agda.TypeChecking.Patterns.Abstract
expandPatternSynonyms | Agda.TypeChecking.Patterns.Abstract
expandPatternSynonyms' | Agda.TypeChecking.Patterns.Abstract
expandProjectedVars | Agda.TypeChecking.MetaVars
expandRecordVar | Agda.TypeChecking.Records
expandRecordVarsRecursively | Agda.TypeChecking.Records
expandTelescopeVar | Agda.TypeChecking.Telescope
explainWhyInScope | Agda.Interaction.EmacsTop
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
ExpRefInfo |
1 (Type/Class) | Agda.Auto.SearchControl
2 (Data Constructor) | Agda.Auto.SearchControl
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
exprToAttribute | Agda.Syntax.Concrete.Attribute
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
ExpTypeSig | Agda.Utils.Haskell.Syntax
ExtendedLam |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
ExtendedLambda | Agda.Interaction.Response
extendedLambdaName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
extendInferredBlock | Agda.Syntax.Concrete.Definitions.Types
extendSolution | Agda.Utils.Warshall
ExtendTel | Agda.Syntax.Internal
ExtLam | Agda.Syntax.Reflected
extLamAbsurd | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
ExtLamInfo |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
extLamModule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
extLamSys | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
extractblkinfos | Agda.Auto.NarrowingSearch
extractPattern | Agda.Syntax.Abstract
extraref | Agda.Auto.SearchControl