eAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eActiveProblems | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eAllowDestructiveUpdate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eAllowedReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eAnonymousModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eAppDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eAssignMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eatNextChar | Agda.Syntax.Parser.LookAhead |
eCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eCheckingWhere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eCompareBlocked | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eCurrentPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
editDistance | Agda.Utils.List |
editDistanceSpec | Agda.Utils.List |
EE | Agda.Auto.Syntax |
eExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
EHCOpts | Agda.Compiler.UHC.Bridge |
eHighlightingLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eHighlightingMethod | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eHighlightingRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eImportPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eInsideDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eInstanceDepth | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
elems | |
1 (Function) | Agda.Utils.HashMap |
2 (Function) | Agda.Utils.Bag |
eLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
eliminateDeadCode | Agda.TypeChecking.DeadCode |
eliminateLiteralPatterns | Agda.Compiler.Treeless.EliminateLiteralPatterns |
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 |
eModuleNestingLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
EmptyRewritePragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
eMutualBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
ensureNPatterns | Agda.TypeChecking.CompiledClause.Compile |
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 |
envClause | 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 |
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 |
envInstanceDepth | 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 |
envPrintMetasBare | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
envRange | 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 |
envUnquoteFlags | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eof | Agda.Syntax.Parser.LexActions |
EpicCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
epicError | Agda.Compiler.Epic.CompileState |
EpicFun | Agda.Compiler.Epic.AuxAST |
ePrintDomainFreePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
eRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
erasedArity | Agda.Compiler.MAlonzo.Compiler |
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 |
eRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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.Interaction.Highlighting.Precise |
3 (Data Constructor) | Agda.Auto.NarrowingSearch |
errorHighlighting | Agda.Interaction.Highlighting.Generate |
ErrorPart | Agda.TypeChecking.Unquote |
ErrorWarnings | Agda.Interaction.Imports |
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 |
eSimplification | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eSolvingConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
etaContract | Agda.TypeChecking.EtaContract |
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 |
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 |
eTerminationCheck | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eUnquoteFlags | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
eUnquoteNormalise | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
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 |
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 |
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.Compiler.Epic.AuxAST |
3 (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 |
extendSolution | Agda.Utils.Warshall |
ExtendTel | Agda.Syntax.Internal |
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 |
extraref | Agda.Auto.SearchControl |