DefinitionsofComponents, filter, toArray, toHashSet, toList, addSimpEntry, containsDecl, foldSimpEntries, foldSimpEntriesM, simpEntries, addTryThisTacticSeqSuggestion, smallErrorMessages, compareArrayLex, compareArraySizeThenLex, elabPattern, filterDiscrTree, filterDiscrTreeM, forEachExprInGoal, forEachExprInGoal', forEachExprInGoalCore, forEachExprInLCtx, forEachExprInLCtx', forEachExprInLCtxCore, forEachExprInLDecl, forEachExprInLDecl', forEachExprInLDeclCore, getAppUpToDefeq, getConclusionDiscrTreeKeys, getUnusedNames, hasSorry, instMonadCacheStateRefT'_aesop, instMonadParentDeclReaderT_aesop, instMonadParentDeclStateRefT'_aesop, isAppOfUpToDefeq, isDefEqReducibleRigid, isEmptyTrie, isHypRedundantReducibleRigid, lBoolOr, partitionGoalsAndMVars, runInMetaState, runMetaMAsCoreM, runTacticCapturingPostState, runTacticMAsMetaM, runTacticMCapturingPostState, runTacticSeqCapturingPostState, runTacticSyntaxAsMetaM, runTacticsCapturingPostState, runTermElabMAsCoreM, setThe, tacticsToMessageData, time, time', updateSimpEntryPriority, withAllTransparencySeqSyntax, withAllTransparencySyntax, withExceptionPrefix, withExceptionTransform, withPPAnalyze | 58 |