| 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 |
| EInterface | |
| 1 (Type/Class) | Agda.Compiler.Epic.Interface |
| 2 (Data Constructor) | Agda.Compiler.Epic.Interface |
| EitherOrBoth | Agda.Utils.Map |
| El | Agda.Syntax.Internal |
| el | Agda.TypeChecking.Primitive |
| elements | Agda.Utils.QuickCheck |
| Elim | Agda.Syntax.Internal |
| ElimCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ElimView | Agda.TypeChecking.Eliminators |
| elimView | Agda.TypeChecking.Eliminators |
| Ellipsis | Agda.Syntax.Concrete |
| Elr | Agda.Auto.Syntax |
| ElseSh | Agda.TypeChecking.Rules.LHS.Unify |
| EmbPrj | Agda.TypeChecking.Serialise |
| emp | Agda.Compiler.JS.Substitution |
| empty | |
| 1 (Function) | Agda.Utils.VarSet |
| 2 (Function) | Agda.Utils.Pretty |
| 3 (Function) | Agda.Utils.Graph |
| 4 (Function) | Agda.Utils.Trie |
| 5 (Function) | Agda.Termination.CallGraph |
| 6 (Function) | Agda.TypeChecking.Pretty |
| emptyC | Agda.Compiler.Epic.Injection |
| 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 |
| emptyUEnv | Agda.TypeChecking.Rules.LHS.Unify |
| emptyUOutput | Agda.TypeChecking.Rules.LHS.Unify |
| 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 |
| envActiveProblems | 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 |
| 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 |
| envRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envSolvingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envTopLevel | 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 |
| eqGroups | Agda.Compiler.Epic.Injection |
| 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 |
| 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 |
| escChr | Agda.Compiler.JS.Parser |
| etaContract | Agda.TypeChecking.EtaContract |
| etaContractBody | Agda.Auto.Convert |
| etaContractRecord | Agda.TypeChecking.Records |
| EtaExpand | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| etaExpand | Agda.Compiler.Epic.Static |
| 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 |
| evaluateCC | Agda.Compiler.Epic.Static |
| evaluateTerm | Agda.Compiler.Epic.Static |
| 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 | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.Compiler.JS.Syntax |
| exp | Agda.Compiler.JS.Parser |
| exp0 | Agda.Compiler.JS.Parser |
| exp1 | Agda.Compiler.JS.Parser |
| exp2 | Agda.Compiler.JS.Parser |
| exp2' | Agda.Compiler.JS.Parser |
| exp3 | Agda.Compiler.JS.Parser |
| exp3' | Agda.Compiler.JS.Parser |
| expandbind | Agda.Auto.NarrowingSearch |
| expandCatchAlls | Agda.TypeChecking.CompiledClause.Compile |
| 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 |
| 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, Agda.Interaction.GhciTop |
| exports | |
| 1 (Function) | Agda.Compiler.JS.Syntax |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| Expr | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Compiler.Epic.AuxAST |
| 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 |
| ExtendedLam | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| ExtendedLambda | Agda.Interaction.MakeCase |
| extendlambdaname | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| extendSolution | Agda.Utils.Warshall |
| ExtendTel | Agda.Syntax.Internal |
| extendWithTelConf | Agda.TypeChecking.Test.Generators |
| extQ | Agda.Utils.Generics |
| extractblkinfos | Agda.Auto.NarrowingSearch |
| extractNthElement | Agda.Utils.List |
| extractNthElement' | Agda.Utils.List |
| extraref | Agda.Auto.SearchControl |