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 |