Agda-2.6.0.1: 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
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
eContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eCurrentCheckpoint | 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
EE | Agda.Auto.Syntax
eExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eGeneralizeMetas | 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
EitherOrBoth | Agda.Utils.Map
El | Agda.Syntax.Internal
el | Agda.TypeChecking.Primitive
el' | Agda.TypeChecking.Primitive
ElaborateGive | Agda.Interaction.InteractionTop
Element | Agda.Utils.Zipper
elemNe | Agda.Utils.NonemptyList
elems |
1 (Function) | Agda.Utils.HashMap
2 (Function) | Agda.Utils.Bag
eLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eligibleForProjectionLike | Agda.TypeChecking.ProjectionLike
Elim |
1 (Type/Class) | Agda.Syntax.Reflected
2 (Type/Class) | Agda.Syntax.Internal
Elim' |
1 (Type/Class) | Agda.Syntax.Reflected
2 (Type/Class) | Agda.Syntax.Internal
ElimCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eliminateCaseDefaults | Agda.Compiler.Treeless.EliminateDefaults
eliminateDeadCode | Agda.TypeChecking.DeadCode
eliminateLiteralPatterns | Agda.Compiler.Treeless.EliminateLiteralPatterns
Elims |
1 (Type/Class) | Agda.Syntax.Reflected
2 (Type/Class) | Agda.Syntax.Internal
ElimType | Agda.TypeChecking.Records
elimView | Agda.TypeChecking.ProjectionLike
elInf | Agda.TypeChecking.Primitive
Ellipsis | Agda.Syntax.Concrete
EllipsisP | Agda.Syntax.Concrete
Elr | Agda.Auto.Syntax
emap | Agda.TypeChecking.Records
embDef | Agda.Syntax.Internal.Defs
EmbPrj | Agda.TypeChecking.Serialise.Base, Agda.TypeChecking.Serialise
eModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eModuleNestingLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
emp | Agda.Compiler.JS.Substitution
Empty | Agda.Utils.Empty
empty |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.HashMap
3 (Function) | Agda.Utils.BiMap
4 (Function) | Agda.Utils.Bag
5 (Function) | Agda.Utils.IntSet.Infinite
6 (Function) | Agda.Utils.Null, Agda.Utils.Trie
7 (Function) | Agda.Interaction.Highlighting.Range
8 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
EmptyAbstract | 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
emptyDict | Agda.TypeChecking.Serialise.Base
emptyFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EmptyGeneralize | Agda.Syntax.Concrete.Definitions
EmptyGeneralize_ | Agda.Interaction.Options.Warnings
emptyGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver
EmptyInstance | Agda.Syntax.Concrete.Definitions
EmptyInstance_ | Agda.Interaction.Options.Warnings
emptyLayout | Agda.Syntax.Parser.Layout
emptyLibFile | Agda.Interaction.Library.Base
EmptyMacro | Agda.Syntax.Concrete.Definitions
EmptyMacro_ | Agda.Interaction.Options.Warnings
emptyMetaInfo | Agda.Syntax.Info
EmptyMutual | Agda.Syntax.Concrete.Definitions
EmptyMutual_ | Agda.Interaction.Options.Warnings
emptyNameSpace | Agda.Syntax.Scope.Base
emptyOB | Agda.TypeChecking.Positivity
emptyPolarities | Agda.TypeChecking.SizedTypes.Syntax
EmptyPostulate | Agda.Syntax.Concrete.Definitions
EmptyPostulate_ | Agda.Interaction.Options.Warnings
EmptyPrimitive | Agda.Syntax.Concrete.Definitions
EmptyPrimitive_ | Agda.Interaction.Options.Warnings
EmptyPrivate | Agda.Syntax.Concrete.Definitions
EmptyPrivate_ | Agda.Interaction.Options.Warnings
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
empty_layout | Agda.Syntax.Parser.Lexer
eMutualBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
enableCaching | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
enableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
enablePhantomTypes | Agda.TypeChecking.Polarity
encode | Agda.TypeChecking.Serialise
encodeFile | Agda.TypeChecking.Serialise
encodeInterface | Agda.TypeChecking.Serialise
encodeModuleName | Agda.Compiler.MAlonzo.Encode
End | Agda.Syntax.Common
end | Agda.Syntax.Parser.LexActions
endBy | Agda.Utils.Parser.ReadP
endBy1 | Agda.Utils.Parser.ReadP
endos | Agda.Termination.Termination
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.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
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
envCheckOptionConsistency | 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
envContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCurrentCheckpoint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envCurrentModule | 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
envGeneralizedVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envGeneralizeMetas | 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
envModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envModuleNestingLevel | 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
envRange | 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
envTerminationCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
envUnquoteFlags | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
Equal | Agda.Syntax.Concrete
equal | Agda.TypeChecking.Rewriting.NonLinMatch
equalAtom | Agda.TypeChecking.Conversion
equalHeadConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
EqualityType | Agda.Syntax.Internal
equalityUnview | Agda.TypeChecking.Monad.Builtin
EqualityView | Agda.Syntax.Internal
equalityView | Agda.TypeChecking.Monad.Builtin
equalLevel | Agda.TypeChecking.Conversion
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
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
eRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
erasedArity | Agda.Compiler.MAlonzo.Compiler
ErasedDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
eraseSBool | Agda.Utils.TypeLits
eraseTerms | Agda.Compiler.Treeless.Erase
eraseUnusedAction | Agda.TypeChecking.CheckInternal
eRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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 (Type/Class) | Agda.Utils.Except
2 (Data Constructor) | Agda.Auto.NarrowingSearch
3 (Data Constructor) | Agda.Interaction.Highlighting.Precise
4 (Data Constructor) | Agda.Interaction.InteractionTop
errorHighlighting | Agda.Interaction.Highlighting.Generate
ErrorNonEmpty | Agda.TypeChecking.Empty
ErrorPart | Agda.TypeChecking.Unquote
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
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
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.TypeChecking.MetaVars
etaExpandMetaSafe | 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
etaInequal | Agda.TypeChecking.Conversion
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.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
evalIn | Agda.Interaction.CommandLine
evalInCurrent | Agda.Interaction.BasicOps
evalInMeta | Agda.Interaction.BasicOps
evalTCM | Agda.TypeChecking.Unquote
evalTerm | Agda.Interaction.CommandLine
EvaluationStrategy | Agda.Syntax.Treeless, Agda.Compiler.Backend
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.InteractionTop
Exception | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
ExceptT | Agda.Utils.Except
ExitCode | Agda.Interaction.CommandLine
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
expandEnvironmentVariables | 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
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
expandWithFunctionCall | Agda.Termination.Inlining
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
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.TypeChecking.Monad, Agda.Compiler.Backend
extendSolution | Agda.Utils.Warshall
ExtendTel | Agda.Syntax.Internal
ExtLam | Agda.Syntax.Reflected
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
extractblkinfos | Agda.Auto.NarrowingSearch
extraref | Agda.Auto.SearchControl