Agda-2.2.10: 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

eatNextChar | Agda.Syntax.Parser.LookAhead
Edge |
1 (Type/Class) | Agda.TypeChecking.Positivity
2 (Data Constructor) | Agda.TypeChecking.Positivity
edges |
1 (Function) | Agda.Utils.Graph
2 (Function) | Agda.Utils.Warshall
EE | Agda.Auto.Syntax
EitherOrBoth | Agda.Utils.Map
El | Agda.Syntax.Internal
el | Agda.TypeChecking.Primitive
elements | Agda.Utils.QuickCheck
Ellipsis | Agda.Syntax.Concrete
Elr | Agda.Auto.Syntax
EmbPrj | Agda.TypeChecking.Serialise
empty |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Utils.Graph
3 (Function) | Agda.Utils.Trie
4 (Function) | Agda.Termination.CallGraph
5 (Function) | Agda.TypeChecking.Pretty
emptyConstraints | Agda.Utils.Warshall
emptyLayout | Agda.Syntax.Parser.Layout
emptyNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
emptyScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
emptyScopeInfo | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
emptySignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
emptySolution | Agda.Utils.Warshall
EmptyTel | Agda.Syntax.Internal
emptyUState | Agda.TypeChecking.Rules.LHS.Unify
empty_layout | Agda.Syntax.Parser.Lexer
enableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
encode | Agda.TypeChecking.Serialise
encodeFile | Agda.TypeChecking.Serialise
encodeModuleName | Agda.Compiler.MAlonzo.Encode
end | Agda.Syntax.Parser.LexActions
endBy | Agda.Utils.ReadP
endBy1 | Agda.Utils.ReadP
endWith | Agda.Syntax.Parser.LexActions
end_ | Agda.Syntax.Parser.LexActions
ensureFileLoaded | Agda.Interaction.GhciTop
enterClosure | Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad
Env | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
envAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envAnonymousModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envDisplayFormsEnabled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envEtaContractImplicit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envImportPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envMutualBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envReifyInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
envReplace | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
eof | Agda.Syntax.Parser.LexActions
Epic | Agda.Interaction.GhciTop
EpicCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
epicError | Agda.Compiler.Epic.CompileState
EpicFun | Agda.Compiler.Epic.AuxAST
eqelr | Agda.Auto.CaseSplit
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
EqRSChain | Agda.Auto.Syntax
EqRSNone | Agda.Auto.Syntax
EqRSPrf1 | Agda.Auto.Syntax
EqRSPrf2 | Agda.Auto.Syntax
EqRSPrf3 | Agda.Auto.Syntax
Equal | Agda.TypeChecking.Rules.LHS.Unify
equalArgs | Agda.TypeChecking.Conversion
equalAtom | Agda.TypeChecking.Conversion
Equality | Agda.TypeChecking.Rules.LHS.Unify
equalLevel | Agda.TypeChecking.Conversion
equals | Agda.Utils.Pretty
equalSort | Agda.TypeChecking.Conversion
equalTerm | Agda.TypeChecking.Conversion
equalType | Agda.TypeChecking.Conversion
Erasure | Agda.Compiler.Epic.Erasure
erasure | Agda.Compiler.Epic.Erasure
ErasureState |
1 (Type/Class) | Agda.Compiler.Epic.Erasure
2 (Data Constructor) | Agda.Compiler.Epic.Erasure
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
errError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
errHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
errInput | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
errMsg | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
Error |
1 (Data Constructor) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
errorTitle | Agda.Interaction.GhciTop
errPos | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
errPrevToken | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop
escape | Agda.Interaction.Highlighting.Vim
escapeContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
etaContract | Agda.TypeChecking.EtaContract
etaContractBody | Agda.Auto.Convert
etaContractRecord | Agda.TypeChecking.Records
etaExpandBlocked | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
etaExpandClause | Agda.TypeChecking.Positivity
etaExpandListeners | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
etaExpandMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
etaExpandMetaSafe | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
etaExpandRecord | Agda.TypeChecking.Records
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
evalIn | Agda.Interaction.CommandLine.CommandLine
evalInCurrent | Agda.Interaction.BasicOps
evalInMeta | Agda.Interaction.BasicOps
evalTerm | Agda.Interaction.CommandLine.CommandLine
everythingBut | Agda.Utils.Generics
everythingInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
everywhereBut' | Agda.Utils.Generics
everywhereButM' | Agda.Utils.Generics
Exception | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
ExceptionT |
1 (Type/Class) | Agda.TypeChecking.Monad.Exception
2 (Data Constructor) | Agda.TypeChecking.Monad.Exception
ExitCode | Agda.Interaction.CommandLine.CommandLine
Exp | Agda.Auto.Syntax
expandbind | Agda.Auto.NarrowingSearch
expandExp | Agda.Auto.Syntax
ExpandHidden | Agda.TypeChecking.Rules.Term
ExpandLast | Agda.TypeChecking.Rules.Term
expandLitPattern | Agda.TypeChecking.Rules.LHS.Split
expandP | Agda.Utils.Permutation
expectFailure | Agda.Utils.QuickCheck
exportedNamesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
Expr |
1 (Type/Class) | Agda.Compiler.Epic.AuxAST
2 (Type/Class) | Agda.Syntax.Concrete
3 (Type/Class) | Agda.Syntax.Abstract
ExpRefInfo |
1 (Type/Class) | Agda.Auto.SearchControl
2 (Data Constructor) | Agda.Auto.SearchControl
ExprHole | Agda.Syntax.Notation
ExprInfo | Agda.Syntax.Info
exprInfo | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop
exprParser |
1 (Function) | Agda.Syntax.Parser.Parser
2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop
ExprRange | Agda.Syntax.Info
ExprSource | Agda.Syntax.Info
ExprView | Agda.Syntax.Concrete.Operators.Parser
exprView | Agda.Syntax.Concrete.Operators.Parser
extendConf | Agda.TypeChecking.Test.Generators
extendSolution | Agda.Utils.Warshall
ExtendTel | Agda.Syntax.Internal
extendWithTelConf | Agda.TypeChecking.Test.Generators
extractblkinfos | Agda.Auto.NarrowingSearch
extractNthElement | Agda.Utils.List
extractNthElement' | Agda.Utils.List
extraref | Agda.Auto.SearchControl