eatNextChar | Agda.Syntax.Parser.LookAhead |
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 | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
2 (Function) | Agda.Utils.Warshall |
edgesFrom | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
edgesTo | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
edgeToLowerBound | Agda.TypeChecking.SizedTypes.WarshallSolver |
edgeToUpperBound | Agda.TypeChecking.SizedTypes.WarshallSolver |
editDistance | Agda.Utils.List |
editDistanceSpec | Agda.Utils.List |
EE | Agda.Auto.Syntax |
EHCOpts | Agda.Compiler.UHC.Bridge |
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 |
elementsUnlessEmpty | Agda.Utils.TestHelpers |
elems | |
1 (Function) | Agda.Utils.HashMap |
2 (Function) | Agda.Utils.Bag |
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 |
ElimFreqs | |
1 (Type/Class) | Agda.TypeChecking.Test.Generators |
2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
elimFreqs | Agda.TypeChecking.Test.Generators |
eliminateDeadCode | Agda.TypeChecking.DeadCode |
Elims | |
1 (Type/Class) | Agda.Syntax.Reflected |
2 (Type/Class) | Agda.Syntax.Internal |
elimView | Agda.TypeChecking.ProjectionLike |
Ellipsis | Agda.Syntax.Concrete |
Elr | Agda.Auto.Syntax |
emap | Agda.TypeChecking.Records |
embDef | Agda.Syntax.Internal.Defs |
EmbPrj | Agda.TypeChecking.Serialise.Base, Agda.TypeChecking.Serialise |
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.Null, Agda.Utils.Trie |
6 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
7 (Function) | Agda.Interaction.Highlighting.Range |
emptyBinds | Agda.Compiler.MAlonzo.Misc |
emptyBound | Agda.TypeChecking.SizedTypes.WarshallSolver |
emptyC | Agda.Compiler.Epic.Injection |
emptyConstraints | Agda.Utils.Warshall |
emptyDict | Agda.TypeChecking.Serialise.Base |
emptyFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
emptyGraphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
emptyLayout | Agda.Syntax.Parser.Layout |
emptyMetaInfo | Agda.Syntax.Info |
emptyNameSpace | Agda.Syntax.Scope.Base |
emptyOB | Agda.TypeChecking.Positivity |
emptyPolarities | Agda.TypeChecking.SizedTypes.Syntax |
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 |
emptySolution | Agda.Utils.Warshall |
EmptyTel | Agda.Syntax.Internal |
empty_layout | Agda.Syntax.Parser.Lexer |
enableCaching | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
enableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
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 |
ensureNoCompiledHaskell | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
enterClosure | |
1 (Function) | Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad |
2 (Function) | Agda.TypeChecking.Reduce.Monad |
EnterSection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Env | Agda.Syntax.Translation.AbstractToConcrete |
envAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envActiveProblems | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envAllowDestructiveUpdate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envAllowedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envAnonymousModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envAppDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envAssignMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envCheckingWhere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envCompareBlocked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envCurrentPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envDisplayFormsEnabled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envEtaContractImplicit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envHighlightingLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envHighlightingMethod | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envHighlightingRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envImportPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envInsideDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envModuleNestingLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envMutualBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envPrintDomainFreePi | 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 |
envSimplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envSolvingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envTerminationCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eof | Agda.Syntax.Parser.LexActions |
Epic | Agda.Interaction.InteractionTop |
EpicCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
epicError | Agda.Compiler.Epic.CompileState |
EpicFun | Agda.Compiler.Epic.AuxAST |
eqelr | Agda.Auto.CaseSplit |
eqFreeVars | Agda.TypeChecking.Rewriting.NonLinMatch |
eqGroups | Agda.Compiler.Epic.Injection |
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 |
eqtLevel | Agda.Syntax.Internal |
eqtLhs | Agda.Syntax.Internal |
eqtName | 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 |
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 |
equals | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
equalSort | Agda.TypeChecking.Conversion |
equalTerm | Agda.TypeChecking.Conversion |
equalTerms | Agda.Compiler.Treeless.Compare |
equalType | Agda.TypeChecking.Conversion |
eraseTerms | Agda.Compiler.Treeless.Erase |
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 |
errInput | 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 |
errorHighlighting | Agda.Interaction.Highlighting.Generate |
ErrorPart | Agda.TypeChecking.Unquote |
errPos | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
errPrevToken | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
errSrcFile | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser |
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 |
etaEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
EtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
etaEqualityToBool | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
EtaExpand | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
etaExpand | Agda.Compiler.Epic.Static |
etaExpandAtRecordType | Agda.TypeChecking.Records |
etaExpandBlocked | Agda.TypeChecking.MetaVars |
etaExpandBoundVar | Agda.TypeChecking.Records |
etaExpandClause | Agda.TypeChecking.Positivity |
etaExpandListeners | Agda.TypeChecking.MetaVars |
etaExpandMeta | Agda.TypeChecking.MetaVars |
etaExpandMetaSafe | Agda.TypeChecking.MetaVars |
etaExpandProjectedVar | Agda.TypeChecking.MetaVars |
etaExpandRecord | Agda.TypeChecking.Records |
etaExpandRecord_ | Agda.TypeChecking.Records |
etaInequal | Agda.TypeChecking.Conversion |
etaOnce | Agda.TypeChecking.EtaContract |
ETel | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
eval | Agda.TypeChecking.SizedTypes.Tests |
evalIn | Agda.Interaction.CommandLine |
evalInCurrent | Agda.Interaction.BasicOps |
evalInMeta | Agda.Interaction.BasicOps |
evalTCM | Agda.TypeChecking.Unquote |
evalTerm | Agda.Interaction.CommandLine |
Evaluate | Agda.Compiler.Epic.Static |
evaluate | Agda.Compiler.Epic.Static |
evaluateCC | Agda.Compiler.Epic.Static |
everyPrefix | Agda.Utils.Trie |
everythingInScope | Agda.Syntax.Scope.Base |
exact | Agda.Interaction.InteractionTop |
Exception | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ExceptionT | |
1 (Type/Class) | Agda.TypeChecking.Monad.Exception |
2 (Data Constructor) | Agda.TypeChecking.Monad.Exception |
ExceptT | Agda.Utils.Except |
exhaustive | Agda.Utils.QuickCheck |
ExitCode | Agda.Interaction.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 |
ExpandBoth | Agda.TypeChecking.Rules.LHS.Problem |
expandCatchAlls | Agda.TypeChecking.CompiledClause.Compile |
expandEnvironmentVariables | Agda.Utils.Environment |
expandExp | Agda.Auto.Syntax |
ExpandHidden | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
expandImplicitPattern | Agda.TypeChecking.Rules.LHS.Implicit |
expandImplicitPattern' | Agda.TypeChecking.Rules.LHS.Implicit |
ExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
expandLitPattern | Agda.TypeChecking.Patterns.Abstract |
expandModuleAssigns | Agda.TypeChecking.Rules.Term |
expandP | Agda.Utils.Permutation |
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 |
expectFailure | Agda.Utils.QuickCheck |
ExplicitStayExplicit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
ExplicitToInstance | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
exportHaskell | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
3 (Type/Class) | Agda.Compiler.Epic.AuxAST |
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 |
extendConf | Agda.TypeChecking.Test.Generators |
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 |
extendSolution | Agda.Utils.Warshall |
ExtendTel | Agda.Syntax.Internal |
extendWithTelConf | Agda.TypeChecking.Test.Generators |
ExtLam | Agda.Syntax.Reflected |
ExtLamInfo | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
extLamNumHidden | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
extLamNumNonHid | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
extractblkinfos | Agda.Auto.NarrowingSearch |
extractNthElement | Agda.Utils.List |
extractNthElement' | Agda.Utils.List |
extraref | Agda.Auto.SearchControl |