From cb2dc7cd45513f6c53ea71818704e564c1c110c2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 22 Aug 2024 14:00:08 +1000 Subject: [PATCH 1/3] chore: cleanup some unused arguments --- Aesop/Tracing.lean | 3 +-- Aesop/Util/Basic.lean | 4 ++-- Aesop/Util/UnorderedArraySet.lean | 4 ++-- 3 files changed, 5 insertions(+), 6 deletions(-) diff --git a/Aesop/Tracing.lean b/Aesop/Tracing.lean index f0275566..c9680e4b 100644 --- a/Aesop/Tracing.lean +++ b/Aesop/Tracing.lean @@ -31,8 +31,7 @@ namespace TraceOption def isEnabled [Monad m] [MonadOptions m] (opt : TraceOption) : m Bool := return opt.option.get (← getOptions) -def withEnabled [Monad m] [MonadWithOptions m] (opt : TraceOption) (k : m α) : - m α := do +def withEnabled [MonadWithOptions m] (opt : TraceOption) (k : m α) : m α := withOptions (λ opts => opt.option.set opts true) k initialize steps : TraceOption ← diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean index 95b78702..b574e415 100644 --- a/Aesop/Util/Basic.lean +++ b/Aesop/Util/Basic.lean @@ -66,12 +66,12 @@ end PersistentHashSet -- TODO upstream; generalise to {m : Type u → Type v}. -- Need to generalise `HashMap.forM` first. -scoped instance {m : Type u → Type u} [BEq α] [Hashable α] [Monad m] : +scoped instance {m : Type u → Type u} [BEq α] [Hashable α] : ForM m (HashMap α β) (α × β) where forM | m, f => m.forM λ a b => f (a, b) -- TODO upstream; generalise to {m : Type u → Type v}. -scoped instance {m : Type u → Type u} [BEq α] [Hashable α] [Monad m] : +scoped instance {m : Type u → Type u} [BEq α] [Hashable α] : ForIn m (HashMap α β) (α × β) where forIn := ForM.forIn diff --git a/Aesop/Util/UnorderedArraySet.lean b/Aesop/Util/UnorderedArraySet.lean index 8da3a2d5..be301867 100644 --- a/Aesop/Util/UnorderedArraySet.lean +++ b/Aesop/Util/UnorderedArraySet.lean @@ -45,7 +45,7 @@ protected def ofSortedArray (xs : Array α) : UnorderedArraySet α := set_option linter.unusedVariables false in /-- O(n*log(n)) -/ -protected def ofArray [ord : Ord α] [Inhabited α] (xs : Array α) : +protected def ofArray [ord : Ord α] (xs : Array α) : UnorderedArraySet α := ⟨xs.sortDedup⟩ @@ -91,7 +91,7 @@ def foldM [Monad m] (f : σ → α → m σ) (init : σ) (s : UnorderedArraySet m σ := s.rep.foldlM f init -instance [Monad m] : ForIn m (UnorderedArraySet α) α where +instance : ForIn m (UnorderedArraySet α) α where forIn s := s.rep.forIn /-- O(n) -/ From 585246c9592a38e2fd7d389732caa3a0d00339a3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 22 Aug 2024 18:00:22 +1000 Subject: [PATCH 2/3] chore: enable lint in CI --- lakefile.toml | 2 + scripts/nolints.json | 1452 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 1454 insertions(+) create mode 100644 scripts/nolints.json diff --git a/lakefile.toml b/lakefile.toml index 96a10fd8..ee87606f 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,6 +1,8 @@ name = "aesop" defaultTargets = ["Aesop"] testDriver = "AesopTest" +lintDriver = "batteries/runLinter" +lintDriverArgs = ["Aesop"] precompileModules = false # We would like to turn this on, but it breaks the Mathlib cache. [[require]] diff --git a/scripts/nolints.json b/scripts/nolints.json new file mode 100644 index 00000000..0bdd0876 --- /dev/null +++ b/scripts/nolints.json @@ -0,0 +1,1452 @@ +[["docBlame", "Aesop.AddRapp"], + ["docBlame", "Aesop.BaseRuleSetMember"], + ["docBlame", "Aesop.BestFirstQueue"], + ["docBlame", "Aesop.BuilderName"], + ["docBlame", "Aesop.CasesPattern"], + ["docBlame", "Aesop.CasesTarget"], + ["docBlame", "Aesop.CasesTarget'"], + ["docBlame", "Aesop.Check"], + ["docBlame", "Aesop.CoreRuleBuilderOutput"], + ["docBlame", "Aesop.CtorNames"], + ["docBlame", "Aesop.DisplayRuleName"], + ["docBlame", "Aesop.ElabM"], + ["docBlame", "Aesop.ElabRuleTerm"], + ["docBlame", "Aesop.EqualUpToIdsM"], + ["docBlame", "Aesop.ExtResult"], + ["docBlame", "Aesop.ExtractScriptM"], + ["docBlame", "Aesop.FIFOQueue"], + ["docBlame", "Aesop.FVarIdSubst"], + ["docBlame", "Aesop.ForwardHypData"], + ["docBlame", "Aesop.GlobalRuleSetMember"], + ["docBlame", "Aesop.Goal"], + ["docBlame", "Aesop.GoalData"], + ["docBlame", "Aesop.GoalId"], + ["docBlame", "Aesop.GoalRef"], + ["docBlame", "Aesop.GoalUnsafe"], + ["docBlame", "Aesop.GoalWithMVars"], + ["docBlame", "Aesop.Index"], + ["docBlame", "Aesop.IndexMatchLocation"], + ["docBlame", "Aesop.IndexMatchResult"], + ["docBlame", "Aesop.IndexingMode"], + ["docBlame", "Aesop.Iteration"], + ["docBlame", "Aesop.LIFOQueue"], + ["docBlame", "Aesop.LocalRuleSetMember"], + ["docBlame", "Aesop.MVarCluster"], + ["docBlame", "Aesop.MVarClusterData"], + ["docBlame", "Aesop.MVarClusterRef"], + ["docBlame", "Aesop.MVarClusterUnsafe"], + ["docBlame", "Aesop.MonadStats"], + ["docBlame", "Aesop.Nanos"], + ["docBlame", "Aesop.NormM"], + ["docBlame", "Aesop.NormRule"], + ["docBlame", "Aesop.NormRuleInfo"], + ["docBlame", "Aesop.NormRuleResult"], + ["docBlame", "Aesop.NormSeqResult"], + ["docBlame", "Aesop.NormSimpContext"], + ["docBlame", "Aesop.NormStep"], + ["docBlame", "Aesop.NormalizationState"], + ["docBlame", "Aesop.Options'"], + ["docBlame", "Aesop.Percent"], + ["docBlame", "Aesop.PhaseName"], + ["docBlame", "Aesop.PhaseSpec"], + ["docBlame", "Aesop.PostponedSafeRule"], + ["docBlame", "Aesop.Queue"], + ["docBlame", "Aesop.Rapp"], + ["docBlame", "Aesop.RappData"], + ["docBlame", "Aesop.RappId"], + ["docBlame", "Aesop.RappRef"], + ["docBlame", "Aesop.RappUnsafe"], + ["docBlame", "Aesop.RegularRule"], + ["docBlame", "Aesop.Rule"], + ["docBlame", "Aesop.RuleBuilder"], + ["docBlame", "Aesop.RuleBuilderInput"], + ["docBlame", "Aesop.RuleFilter"], + ["docBlame", "Aesop.RuleName"], + ["docBlame", "Aesop.RulePatternInstantiation"], + ["docBlame", "Aesop.RuleResult"], + ["docBlame", "Aesop.RuleSetName"], + ["docBlame", "Aesop.RuleSetNameFilter"], + ["docBlame", "Aesop.RuleStats"], + ["docBlame", "Aesop.RuleStatsTotals"], + ["docBlame", "Aesop.RuleTacDescr"], + ["docBlame", "Aesop.RuleTerm"], + ["docBlame", "Aesop.SafeExpansionM"], + ["docBlame", "Aesop.SafeRule"], + ["docBlame", "Aesop.SafeRuleInfo"], + ["docBlame", "Aesop.SafeRuleResult"], + ["docBlame", "Aesop.SafeRulesResult"], + ["docBlame", "Aesop.Safety"], + ["docBlame", "Aesop.SaturateM"], + ["docBlame", "Aesop.ScopeName"], + ["docBlame", "Aesop.ScriptGenerated"], + ["docBlame", "Aesop.ScriptM"], + ["docBlame", "Aesop.ScriptT"], + ["docBlame", "Aesop.SearchM"], + ["docBlame", "Aesop.SimpResult"], + ["docBlame", "Aesop.Stats"], + ["docBlame", "Aesop.StatsArray"], + ["docBlame", "Aesop.StatsExtension"], + ["docBlame", "Aesop.StatsExtensionEntry"], + ["docBlame", "Aesop.StatsExtensionState"], + ["docBlame", "Aesop.StatsRef"], + ["docBlame", "Aesop.StatsReport"], + ["docBlame", "Aesop.SyntaxMap"], + ["docBlame", "Aesop.SyntaxRewrite"], + ["docBlame", "Aesop.SyntaxRewriteMap"], + ["docBlame", "Aesop.TraceOption"], + ["docBlame", "Aesop.Tree"], + ["docBlame", "Aesop.TreeM"], + ["docBlame", "Aesop.TreeRef"], + ["docBlame", "Aesop.TreeSpec"], + ["docBlame", "Aesop.UnfoldRule"], + ["docBlame", "Aesop.UnionFind"], + ["docBlame", "Aesop.UnorderedArraySet"], + ["docBlame", "Aesop.UnsafeQueue"], + ["docBlame", "Aesop.UnsafeQueueEntry"], + ["docBlame", "Aesop.UnsafeRule"], + ["docBlame", "Aesop.UnsafeRuleInfo"], + ["docBlame", "Aesop.addLetDeclsToSimpTheoremsUnlessZetaDelta"], + ["docBlame", "Aesop.addRapps"], + ["docBlame", "Aesop.applyPostponedSafeRule"], + ["docBlame", "Aesop.applyS"], + ["docBlame", "Aesop.assertHypothesisS"], + ["docBlame", "Aesop.builtinRuleSetName"], + ["docBlame", "Aesop.builtinRuleSetNames"], + ["docBlame", "Aesop.checkAndTraceScript"], + ["docBlame", "Aesop.checkElabRuleTermForSimp"], + ["docBlame", "Aesop.checkGoalLimit"], + ["docBlame", "Aesop.checkInvariantsIfEnabled"], + ["docBlame", "Aesop.checkRappLimit"], + ["docBlame", "Aesop.checkRenderedScriptIfEnabled"], + ["docBlame", "Aesop.checkRootUnprovable"], + ["docBlame", "Aesop.checkSimp"], + ["docBlame", "Aesop.clearForwardImplDetailHyps"], + ["docBlame", "Aesop.clearS"], + ["docBlame", "Aesop.collectStatsOption"], + ["docBlame", "Aesop.commandDeclare_aesop_exception___"], + ["docBlame", "Aesop.ctorNamesToInductionAlts"], + ["docBlame", "Aesop.ctorNamesToRCasesPats"], + ["docBlame", "Aesop.declaredRuleSetsRef"], + ["docBlame", "Aesop.defaultNormPenalty"], + ["docBlame", "Aesop.defaultRuleSetName"], + ["docBlame", "Aesop.defaultSafePenalty"], + ["docBlame", "Aesop.defaultSimpRulePriority"], + ["docBlame", "Aesop.defaultSuccessProbability"], + ["docBlame", "Aesop.discrTreeConfig"], + ["docBlame", "Aesop.«doElemAesop_trace![_]__»"], + ["docBlame", "Aesop.«doElemAesop_trace[_]___»"], + ["docBlame", "Aesop.elabGlobalRuleIdent"], + ["docBlame", "Aesop.elabGlobalRuleIdent?"], + ["docBlame", "Aesop.elabInductiveRuleIdent"], + ["docBlame", "Aesop.elabInductiveRuleIdent?"], + ["docBlame", "Aesop.elabPattern"], + ["docBlame", "Aesop.elabRuleTermForApplyLike"], + ["docBlame", "Aesop.elabRuleTermForApplyLikeCore"], + ["docBlame", "Aesop.elabRuleTermForApplyLikeMetaM"], + ["docBlame", "Aesop.elabRuleTermForSimpCore"], + ["docBlame", "Aesop.elabRuleTermForSimpMetaM"], + ["docBlame", "Aesop.elabSimpTheorems"], + ["docBlame", "Aesop.enqueueGoals"], + ["docBlame", "Aesop.evalAesop"], + ["docBlame", "Aesop.exceptRuleResultToEmoji"], + ["docBlame", "Aesop.expandGoal"], + ["docBlame", "Aesop.expandNextGoal"], + ["docBlame", "Aesop.expandSafePrefix"], + ["docBlame", "Aesop.exprsEqualUpToIds"], + ["docBlame", "Aesop.exprsEqualUpToIds'"], + ["docBlame", "Aesop.extractProof"], + ["docBlame", "Aesop.extractSafePrefix"], + ["docBlame", "Aesop.extractSafePrefixScript"], + ["docBlame", "Aesop.extractScript"], + ["docBlame", "Aesop.finalizeProof"], + ["docBlame", "Aesop.finishIfProven"], + ["docBlame", "Aesop.forEachExprInGoal"], + ["docBlame", "Aesop.forEachExprInGoal'"], + ["docBlame", "Aesop.forEachExprInGoalCore"], + ["docBlame", "Aesop.freeTree"], + ["docBlame", "Aesop.getAllIntroducedMVars"], + ["docBlame", "Aesop.getAndIncrementNextGoalId"], + ["docBlame", "Aesop.getAndIncrementNextRappId"], + ["docBlame", "Aesop.getConclusionDiscrTreeKeys"], + ["docBlame", "Aesop.getConstDiscrTreeKeys"], + ["docBlame", "Aesop.getDeclaredRuleSets"], + ["docBlame", "Aesop.getDefaultRuleSetNames"], + ["docBlame", "Aesop.getForwardHypData"], + ["docBlame", "Aesop.getForwardImplDetailHyps"], + ["docBlame", "Aesop.getGoal"], + ["docBlame", "Aesop.getIteration"], + ["docBlame", "Aesop.getMVarDependencies"], + ["docBlame", "Aesop.getNewFVars"], + ["docBlame", "Aesop.getProof?"], + ["docBlame", "Aesop.getRootGoal"], + ["docBlame", "Aesop.getRootMVarCluster"], + ["docBlame", "Aesop.getRootMVarId"], + ["docBlame", "Aesop.getRootMetaState"], + ["docBlame", "Aesop.getRuleNameForExpr"], + ["docBlame", "Aesop.getSingleGoal"], + ["docBlame", "Aesop.getStatsArray"], + ["docBlame", "Aesop.getTree"], + ["docBlame", "Aesop.handleNonfatalError"], + ["docBlame", "Aesop.hasSorry"], + ["docBlame", "Aesop.incrementIteration"], + ["docBlame", "Aesop.incrementNumGoals"], + ["docBlame", "Aesop.incrementNumRapps"], + ["docBlame", "Aesop.instForInHashMapProd_aesop"], + ["docBlame", "Aesop.instForMHashMapProd_aesop"], + ["docBlame", "Aesop.introsS"], + ["docBlame", "Aesop.introsUnfoldingS"], + ["docBlame", "Aesop.isAppOfUpToDefeq"], + ["docBlame", "Aesop.isEmptyTrie"], + ["docBlame", "Aesop.isForwardImplDetailHyp"], + ["docBlame", "Aesop.isForwardOrDestructRuleName"], + ["docBlame", "Aesop.isSafeExpansionFailedException"], + ["docBlame", "Aesop.isStatsCollectionEnabled"], + ["docBlame", "Aesop.isStatsCollectionOrTracingEnabled"], + ["docBlame", "Aesop.isStatsTracingEnabled"], + ["docBlame", "Aesop.localRuleSetName"], + ["docBlame", "Aesop.matchByTactic?"], + ["docBlame", "Aesop.matchRulePatterns"], + ["docBlame", "Aesop.matchRulePatternsCore"], + ["docBlame", "Aesop.mkCtorNames"], + ["docBlame", "Aesop.mkInitialTree"], + ["docBlame", "Aesop.mkLocalRuleSet"], + ["docBlame", "Aesop.mkNormSimpScriptStep"], + ["docBlame", "Aesop.mkSimpArgs"], + ["docBlame", "Aesop.mkUnfoldSimpContext"], + ["docBlame", "Aesop.modifyCurrentStats"], + ["docBlame", "Aesop.modifyTree"], + ["docBlame", "Aesop.mvarIdToSubgoal"], + ["docBlame", "Aesop.newNodeEmoji"], + ["docBlame", "Aesop.nextActiveGoal"], + ["docBlame", "Aesop.nodeProvedEmoji"], + ["docBlame", "Aesop.nodeUnknownEmoji"], + ["docBlame", "Aesop.nodeUnprovableEmoji"], + ["docBlame", "Aesop.normSimp"], + ["docBlame", "Aesop.normSimpCore"], + ["docBlame", "Aesop.normUnfold"], + ["docBlame", "Aesop.normUnfoldCore"], + ["docBlame", "Aesop.normalizeGoalIfNecessary"], + ["docBlame", "Aesop.normalizeGoalMVar"], + ["docBlame", "Aesop.optNormRuleResultEmoji"], + ["docBlame", "Aesop.optNormRuleResultToNormSeqResult"], + ["docBlame", "Aesop.optimizeScript"], + ["docBlame", "Aesop.optimizeSyntax"], + ["docBlame", "Aesop.optimizeSyntaxWith"], + ["docBlame", "Aesop.popGoal?"], + ["docBlame", "Aesop.postTraverseDown"], + ["docBlame", "Aesop.postTraverseUp"], + ["docBlame", "Aesop.postponedSafeRuleSuccessProbability"], + ["docBlame", "Aesop.preTraverseDown"], + ["docBlame", "Aesop.preTraverseUp"], + ["docBlame", "Aesop.preprocessRule"], + ["docBlame", "Aesop.profiling"], + ["docBlame", "Aesop.profilingRule"], + ["docBlame", "Aesop.profilingRuleSelection"], + ["docBlame", "Aesop.recordScriptGenerated"], + ["docBlame", "Aesop.recordScriptStep"], + ["docBlame", "Aesop.recordScriptSteps"], + ["docBlame", "Aesop.recordStatsIfEnabled"], + ["docBlame", "Aesop.registerTraceOption"], + ["docBlame", "Aesop.renameInaccessibleFVarsS"], + ["docBlame", "Aesop.replaceFVarS"], + ["docBlame", "Aesop.resolveTraceOption"], + ["docBlame", "Aesop.ruleErrorEmoji"], + ["docBlame", "Aesop.ruleFailureEmoji"], + ["docBlame", "Aesop.rulePostponedEmoji"], + ["docBlame", "Aesop.ruleProvedEmoji"], + ["docBlame", "Aesop.ruleSkippedEmoji"], + ["docBlame", "Aesop.ruleSuccessEmoji"], + ["docBlame", "Aesop.runFirstNormRule"], + ["docBlame", "Aesop.runFirstSafeRule"], + ["docBlame", "Aesop.runFirstUnsafeRule"], + ["docBlame", "Aesop.runMetaMAsCoreM"], + ["docBlame", "Aesop.runNormRule"], + ["docBlame", "Aesop.runNormRuleTac"], + ["docBlame", "Aesop.runNormSteps"], + ["docBlame", "Aesop.runRegularRuleCore"], + ["docBlame", "Aesop.runRegularRuleTac"], + ["docBlame", "Aesop.runRuleTac"], + ["docBlame", "Aesop.runSafeRule"], + ["docBlame", "Aesop.runTacticCapturingPostState"], + ["docBlame", "Aesop.runTacticMAsElabM"], + ["docBlame", "Aesop.runTacticMAsMetaM"], + ["docBlame", "Aesop.runTacticMAsTermElabM"], + ["docBlame", "Aesop.runTacticMCapturingPostState"], + ["docBlame", "Aesop.runTacticSeqCapturingPostState"], + ["docBlame", "Aesop.runTacticSyntaxAsMetaM"], + ["docBlame", "Aesop.runTacticsCapturingPostState"], + ["docBlame", "Aesop.runTermElabMAsCoreM"], + ["docBlame", "Aesop.runUnsafeRule"], + ["docBlame", "Aesop.safeExpansionFailedException"], + ["docBlame", "Aesop.safeExpansionFailedExceptionId"], + ["docBlame", "Aesop.saturate"], + ["docBlame", "Aesop.saturateCore"], + ["docBlame", "Aesop.search"], + ["docBlame", "Aesop.searchLoop"], + ["docBlame", "Aesop.selectNormRules"], + ["docBlame", "Aesop.selectSafeRules"], + ["docBlame", "Aesop.selectUnsafeRules"], + ["docBlame", "Aesop.setMaxRuleApplicationDepthReached"], + ["docBlame", "Aesop.setThe"], + ["docBlame", "Aesop.setTree"], + ["docBlame", "Aesop.shouldParsePriorities"], + ["docBlame", "Aesop.simpAll"], + ["docBlame", "Aesop.simpGoal"], + ["docBlame", "Aesop.simpGoalWithAllHypotheses"], + ["docBlame", "Aesop.sortRuleStatsTotals"], + ["docBlame", "Aesop.splitFirstHypothesisS?"], + ["docBlame", "Aesop.splitTargetS?"], + ["docBlame", "Aesop.statsExtension"], + ["docBlame", "Aesop.straightLineExt"], + ["docBlame", "Aesop.straightLineExtProgress"], + ["docBlame", "Aesop.straightLineExtS"], + ["docBlame", "Aesop.tacticAesop_unfold_"], + ["docBlame", "Aesop.tacticAesop_unfold_At_"], + ["docBlame", "Aesop.tacticStatesEqualUpToIds"], + ["docBlame", "Aesop.tacticStatesEqualUpToIds'"], + ["docBlame", "Aesop.tacticsToMessageData"], + ["docBlame", "Aesop.throwAesopEx"], + ["docBlame", "Aesop.time"], + ["docBlame", "Aesop.time'"], + ["docBlame", "Aesop.traceScript"], + ["docBlame", "Aesop.traceSimpTheoremTreeContents"], + ["docBlame", "Aesop.traceSimpTheorems"], + ["docBlame", "Aesop.traceTree"], + ["docBlame", "Aesop.traverseDown"], + ["docBlame", "Aesop.traverseUp"], + ["docBlame", "Aesop.tree"], + ["docBlame", "Aesop.treeImpl"], + ["docBlame", "Aesop.tryCasesS"], + ["docBlame", "Aesop.tryClearManyS"], + ["docBlame", "Aesop.tryClearS"], + ["docBlame", "Aesop.tryExactFVarS"], + ["docBlame", "Aesop.unassignedMVarsEqualUptoIds"], + ["docBlame", "Aesop.unassignedMVarsEqualUptoIds'"], + ["docBlame", "Aesop.unfoldMany"], + ["docBlame", "Aesop.unfoldManyAt"], + ["docBlame", "Aesop.unfoldManyAtS"], + ["docBlame", "Aesop.unfoldManyCore"], + ["docBlame", "Aesop.unfoldManyStar"], + ["docBlame", "Aesop.unfoldManyStarS"], + ["docBlame", "Aesop.unfoldManyTarget"], + ["docBlame", "Aesop.unfoldManyTargetS"], + ["docBlame", "Aesop.unificationGoalPenalty"], + ["docBlame", "Aesop.unindexPredicate?"], + ["docBlame", "Aesop.updateSimpEntryPriority"], + ["docBlame", "Aesop.wasMaxRuleApplicationDepthReached"], + ["docBlame", "Aesop.withAesopTraceNode"], + ["docBlame", "Aesop.withAllTransparencySeqSyntax"], + ["docBlame", "Aesop.withAllTransparencySyntax"], + ["docBlame", "Aesop.withConstAesopTraceNode"], + ["docBlame", "Aesop.withExceptionPrefix"], + ["docBlame", "Aesop.withExceptionTransform"], + ["docBlame", "Aesop.withFullElaboration"], + ["docBlame", "Aesop.withNormTraceNode"], + ["docBlame", "Aesop.withOptScriptStep"], + ["docBlame", "Aesop.withRuleTraceNode"], + ["docBlame", "Aesop.withScriptStep"], + ["docBlame", "Aesop.withTransparencySeqSyntax"], + ["docBlame", "Aesop.withTransparencySyntax"], + ["docBlame", "Aesop.AddRapp.appliedRule"], + ["docBlame", "Aesop.AddRapp.parent"], + ["docBlame", "Aesop.AddRapp.successProbability"], + ["docBlame", "Aesop.BaseRuleSet.add"], + ["docBlame", "Aesop.BaseRuleSet.contains"], + ["docBlame", "Aesop.BaseRuleSet.empty"], + ["docBlame", "Aesop.BaseRuleSet.erase"], + ["docBlame", "Aesop.BaseRuleSet.merge"], + ["docBlame", "Aesop.BaseRuleSet.trace"], + ["docBlame", "Aesop.BaseRuleSetMember.name"], + ["docBlame", "Aesop.BestFirstQueue.ActiveGoal"], + ["docBlame", "Aesop.BestFirstQueue.addGoals"], + ["docBlame", "Aesop.BestFirstQueue.init"], + ["docBlame", "Aesop.BestFirstQueue.popGoal"], + ["docBlame", "Aesop.BuiltinRules.SubstitutableEq"], + ["docBlame", "Aesop.BuiltinRules.SubstitutableHyp"], + ["docBlame", "Aesop.BuiltinRules.applyHyp"], + ["docBlame", "Aesop.BuiltinRules.applyHyps"], + ["docBlame", "Aesop.BuiltinRules.assumption"], + ["docBlame", "Aesop.BuiltinRules.destructProducts"], + ["docBlame", "Aesop.BuiltinRules.destructProductsCore"], + ["docBlame", "Aesop.BuiltinRules.ext"], + ["docBlame", "Aesop.BuiltinRules.extCore"], + ["docBlame", "Aesop.BuiltinRules.getSubstitutableEqs"], + ["docBlame", "Aesop.BuiltinRules.getSubstitutableHyp"], + ["docBlame", "Aesop.BuiltinRules.intros"], + ["docBlame", "Aesop.BuiltinRules.rfl"], + ["docBlame", "Aesop.BuiltinRules.splitHypotheses"], + ["docBlame", "Aesop.BuiltinRules.splitHypothesesCore"], + ["docBlame", "Aesop.BuiltinRules.splitTarget"], + ["docBlame", "Aesop.BuiltinRules.subst"], + ["docBlame", "Aesop.BuiltinRules.substFVars"], + ["docBlame", "Aesop.CasesPattern.check"], + ["docBlame", "Aesop.CasesPattern.toExpr"], + ["docBlame", "Aesop.CasesPattern.toIndexingMode"], + ["docBlame", "Aesop.CasesTarget.toCasesTarget'"], + ["docBlame", "Aesop.Check.all"], + ["docBlame", "Aesop.Check.get"], + ["docBlame", "Aesop.Check.isEnabled"], + ["docBlame", "Aesop.Check.name"], + ["docBlame", "Aesop.Check.proofReconstruction"], + ["docBlame", "Aesop.Check.rules"], + ["docBlame", "Aesop.Check.script"], + ["docBlame", "Aesop.Check.toOption"], + ["docBlame", "Aesop.Check.tree"], + ["docBlame", "Aesop.CoreRuleBuilderOutput.builderName"], + ["docBlame", "Aesop.CoreRuleBuilderOutput.indexingMode"], + ["docBlame", "Aesop.CoreRuleBuilderOutput.pattern?"], + ["docBlame", "Aesop.CoreRuleBuilderOutput.ruleExprName"], + ["docBlame", "Aesop.CoreRuleBuilderOutput.scopeName"], + ["docBlame", "Aesop.CoreRuleBuilderOutput.tac"], + ["docBlame", "Aesop.CtorNames.args"], + ["docBlame", "Aesop.CtorNames.ctor"], + ["docBlame", "Aesop.CtorNames.mkFreshArgNames"], + ["docBlame", "Aesop.CtorNames.toAltVarNames"], + ["docBlame", "Aesop.CtorNames.toInductionAlt"], + ["docBlame", "Aesop.CtorNames.toInductionAltLHS"], + ["docBlame", "Aesop.CtorNames.toRCasesPat"], + ["docBlame", "Aesop.ElabM.Context"], + ["docBlame", "Aesop.ElabM.run"], + ["docBlame", "Aesop.ElabM.runForwardElab"], + ["docBlame", "Aesop.ElabRuleTerm.expr"], + ["docBlame", "Aesop.ElabRuleTerm.name"], + ["docBlame", "Aesop.ElabRuleTerm.ofElaboratedTerm"], + ["docBlame", "Aesop.ElabRuleTerm.scope"], + ["docBlame", "Aesop.ElabRuleTerm.toRuleTerm"], + ["docBlame", "Aesop.EqualUpToIds.GoalContext"], + ["docBlame", "Aesop.EqualUpToIds.MVarValue"], + ["docBlame", "Aesop.EqualUpToIds.equalCommonLMVars?"], + ["docBlame", "Aesop.EqualUpToIds.equalCommonMVars?"], + ["docBlame", "Aesop.EqualUpToIds.exprsEqualUpToIdsCore"], + ["docBlame", "Aesop.EqualUpToIds.levelsEqualUpToIdsCore"], + ["docBlame", "Aesop.EqualUpToIds.readAllowAssignmentDiff"], + ["docBlame", "Aesop.EqualUpToIds.readCommonMCtx?"], + ["docBlame", "Aesop.EqualUpToIds.readMCtx₁"], + ["docBlame", "Aesop.EqualUpToIds.readMCtx₂"], + ["docBlame", "Aesop.EqualUpToIds.tacticStatesEqualUpToIdsCore"], + ["docBlame", "Aesop.EqualUpToIds.unassignedMVarsEqualUpToIdsCore"], + ["docBlame", "Aesop.EqualUpToIdsM.Context"], + ["docBlame", "Aesop.EqualUpToIdsM.State"], + ["docBlame", "Aesop.EqualUpToIdsM.run"], + ["docBlame", "Aesop.EqualUpToIdsM.run'"], + ["docBlame", "Aesop.ExtResult.commonFVarIds"], + ["docBlame", "Aesop.ExtResult.depth"], + ["docBlame", "Aesop.ExtResult.goals"], + ["docBlame", "Aesop.ExtractScript.lazyStepToStep"], + ["docBlame", "Aesop.ExtractScript.lazyStepsToSteps"], + ["docBlame", "Aesop.ExtractScript.recordLazySteps"], + ["docBlame", "Aesop.ExtractScript.recordStep"], + ["docBlame", "Aesop.ExtractScript.visitGoal"], + ["docBlame", "Aesop.ExtractScript.visitRapp"], + ["docBlame", "Aesop.ExtractScriptM.Context"], + ["docBlame", "Aesop.ExtractScriptM.State"], + ["docBlame", "Aesop.ExtractScriptM.run"], + ["docBlame", "Aesop.FIFOQueue.addGoals"], + ["docBlame", "Aesop.FIFOQueue.goals"], + ["docBlame", "Aesop.FIFOQueue.init"], + ["docBlame", "Aesop.FIFOQueue.popGoal"], + ["docBlame", "Aesop.FIFOQueue.pos"], + ["docBlame", "Aesop.FVarIdSubst.append"], + ["docBlame", "Aesop.FVarIdSubst.apply"], + ["docBlame", "Aesop.FVarIdSubst.applyToLocalDecl"], + ["docBlame", "Aesop.FVarIdSubst.codomain"], + ["docBlame", "Aesop.FVarIdSubst.contains"], + ["docBlame", "Aesop.FVarIdSubst.domain"], + ["docBlame", "Aesop.FVarIdSubst.empty"], + ["docBlame", "Aesop.FVarIdSubst.erase"], + ["docBlame", "Aesop.FVarIdSubst.find?"], + ["docBlame", "Aesop.FVarIdSubst.get"], + ["docBlame", "Aesop.FVarIdSubst.insert"], + ["docBlame", "Aesop.FVarIdSubst.isEmpty"], + ["docBlame", "Aesop.FVarIdSubst.map"], + ["docBlame", "Aesop.FVarIdSubst.ofFVarSubst?"], + ["docBlame", "Aesop.FVarIdSubst.ofFVarSubstIgnoringNonFVarIds"], + ["docBlame", "Aesop.ForwardHypData.containsTypeUpToIds"], + ["docBlame", "Aesop.Frontend.AttrConfig"], + ["docBlame", "Aesop.Frontend.BuilderOption"], + ["docBlame", "Aesop.Frontend.DBuilderName"], + ["docBlame", "Aesop.Frontend.Feature"], + ["docBlame", "Aesop.Frontend.Priority"], + ["docBlame", "Aesop.Frontend.RuleConfig"], + ["docBlame", "Aesop.Frontend.RuleExpr"], + ["docBlame", "Aesop.Frontend.RuleSets"], + ["docBlame", "Aesop.Frontend.TacticConfig"], + ["docBlame", "Aesop.Frontend.addBuilderOption"], + ["docBlame", "Aesop.Frontend.addGlobalRule"], + ["docBlame", "Aesop.Frontend.addLocalImplications"], + ["docBlame", "Aesop.Frontend.checkRuleSetNotDeclared"], + ["docBlame", "Aesop.Frontend.declareRuleSet"], + ["docBlame", "Aesop.Frontend.declareRuleSetUnchecked"], + ["docBlame", "Aesop.Frontend.elabAdditionalForwardRules"], + ["docBlame", "Aesop.Frontend.elabBoolLit"], + ["docBlame", "Aesop.Frontend.elabConfigUnsafe"], + ["docBlame", "Aesop.Frontend.elabForwardRule"], + ["docBlame", "Aesop.Frontend.elabForwardRuleSet"], + ["docBlame", "Aesop.Frontend.elabForwardRuleSetCore"], + ["docBlame", "Aesop.Frontend.elabGlobalRuleSets"], + ["docBlame", "Aesop.Frontend.elabOptions"], + ["docBlame", "Aesop.Frontend.elabSimpConfig"], + ["docBlame", "Aesop.Frontend.elabSimpConfigCtx"], + ["docBlame", "Aesop.Frontend.elabSingleIndexingMode"], + ["docBlame", "Aesop.Frontend.elabTransparency"], + ["docBlame", "Aesop.Frontend.eraseGlobalRules"], + ["docBlame", "Aesop.Frontend.evalSaturate"], + ["docBlame", "Aesop.Frontend.extensionDescr"], + ["docBlame", "Aesop.Frontend.getDeclaredGlobalRuleSets"], + ["docBlame", "Aesop.Frontend.getDefaultGlobalRuleSets"], + ["docBlame", "Aesop.Frontend.getGlobalRuleSet"], + ["docBlame", "Aesop.Frontend.getGlobalRuleSetData"], + ["docBlame", "Aesop.Frontend.getGlobalRuleSetFromData"], + ["docBlame", "Aesop.Frontend.getGlobalRuleSets"], + ["docBlame", "Aesop.Frontend.isImplication"], + ["docBlame", "Aesop.Frontend.isRuleSetDeclared"], + ["docBlame", "Aesop.Frontend.mkForwardOptions"], + ["docBlame", "Aesop.Frontend.mkHypForwardRule"], + ["docBlame", "Aesop.Frontend.mkHypImplicationRule?"], + ["docBlame", "Aesop.Frontend.modifyGetGlobalRuleSet"], + ["docBlame", "Aesop.Frontend.modifyGlobalRuleSet"], + ["docBlame", "Aesop.Frontend.tacticForward?___"], + ["docBlame", "Aesop.Frontend.tacticForward___"], + ["docBlame", "Aesop.Frontend.tacticSaturate?_____"], + ["docBlame", "Aesop.Frontend.tacticSaturate_____"], + ["docBlame", "Aesop.GlobalRuleSet.contains"], + ["docBlame", "Aesop.GlobalRuleSet.empty"], + ["docBlame", "Aesop.GlobalRuleSet.erase"], + ["docBlame", "Aesop.GlobalRuleSet.modifyBase"], + ["docBlame", "Aesop.GlobalRuleSet.modifyBaseM"], + ["docBlame", "Aesop.GlobalRuleSet.onBase"], + ["docBlame", "Aesop.GlobalRuleSet.onBaseM"], + ["docBlame", "Aesop.GlobalRuleSet.trace"], + ["docBlame", "Aesop.GlobalRuleSetMember.name"], + ["docBlame", "Aesop.Goal.addedInIteration"], + ["docBlame", "Aesop.Goal.children"], + ["docBlame", "Aesop.Goal.currentGoal"], + ["docBlame", "Aesop.Goal.currentGoalAndMetaState"], + ["docBlame", "Aesop.Goal.depth"], + ["docBlame", "Aesop.Goal.elim"], + ["docBlame", "Aesop.Goal.extractProof"], + ["docBlame", "Aesop.Goal.extractSafePrefix"], + ["docBlame", "Aesop.Goal.failedRapps"], + ["docBlame", "Aesop.Goal.firstProvenRapp?"], + ["docBlame", "Aesop.Goal.hasMVar"], + ["docBlame", "Aesop.Goal.hasProvableRapp"], + ["docBlame", "Aesop.Goal.hasSafeRapp"], + ["docBlame", "Aesop.Goal.id"], + ["docBlame", "Aesop.Goal.isActive"], + ["docBlame", "Aesop.Goal.isExhausted"], + ["docBlame", "Aesop.Goal.isForcedUnprovable"], + ["docBlame", "Aesop.Goal.isIrrelevant"], + ["docBlame", "Aesop.Goal.isIrrelevantNoCache"], + ["docBlame", "Aesop.Goal.isNormal"], + ["docBlame", "Aesop.Goal.isProvenByNormalizationNoCache"], + ["docBlame", "Aesop.Goal.isProvenByRuleApplicationNoCache"], + ["docBlame", "Aesop.Goal.isProvenNoCache"], + ["docBlame", "Aesop.Goal.isRoot"], + ["docBlame", "Aesop.Goal.isUnprovableNoCache"], + ["docBlame", "Aesop.Goal.isUnsafeExhausted"], + ["docBlame", "Aesop.Goal.lastExpandedInIteration"], + ["docBlame", "Aesop.Goal.mk"], + ["docBlame", "Aesop.Goal.modify"], + ["docBlame", "Aesop.Goal.mvars"], + ["docBlame", "Aesop.Goal.normalizationState"], + ["docBlame", "Aesop.Goal.origin"], + ["docBlame", "Aesop.Goal.originalGoalId"], + ["docBlame", "Aesop.Goal.parent"], + ["docBlame", "Aesop.Goal.parentMetaState"], + ["docBlame", "Aesop.Goal.parentRapp?"], + ["docBlame", "Aesop.Goal.postNormGoal?"], + ["docBlame", "Aesop.Goal.postNormGoalAndMetaState?"], + ["docBlame", "Aesop.Goal.preNormGoal"], + ["docBlame", "Aesop.Goal.priority"], + ["docBlame", "Aesop.Goal.runMetaMInParentState"], + ["docBlame", "Aesop.Goal.runMetaMInParentState'"], + ["docBlame", "Aesop.Goal.runMetaMInPostNormState"], + ["docBlame", "Aesop.Goal.runMetaMInPostNormState'"], + ["docBlame", "Aesop.Goal.runMetaMModifyingParentState"], + ["docBlame", "Aesop.Goal.safeRapps"], + ["docBlame", "Aesop.Goal.setAddedInIteration"], + ["docBlame", "Aesop.Goal.setChildren"], + ["docBlame", "Aesop.Goal.setDepth"], + ["docBlame", "Aesop.Goal.setFailedRapps"], + ["docBlame", "Aesop.Goal.setId"], + ["docBlame", "Aesop.Goal.setIsForcedUnprovable"], + ["docBlame", "Aesop.Goal.setIsIrrelevant"], + ["docBlame", "Aesop.Goal.setLastExpandedInIteration"], + ["docBlame", "Aesop.Goal.setMVars"], + ["docBlame", "Aesop.Goal.setNormalizationState"], + ["docBlame", "Aesop.Goal.setOrigin"], + ["docBlame", "Aesop.Goal.setParent"], + ["docBlame", "Aesop.Goal.setPreNormGoal"], + ["docBlame", "Aesop.Goal.setState"], + ["docBlame", "Aesop.Goal.setSuccessProbability"], + ["docBlame", "Aesop.Goal.setUnsafeQueue"], + ["docBlame", "Aesop.Goal.setUnsafeRulesSelected"], + ["docBlame", "Aesop.Goal.state"], + ["docBlame", "Aesop.Goal.stateNoCache"], + ["docBlame", "Aesop.Goal.successProbability"], + ["docBlame", "Aesop.Goal.traceMetadata"], + ["docBlame", "Aesop.Goal.traceTree"], + ["docBlame", "Aesop.Goal.traceTreeCore"], + ["docBlame", "Aesop.Goal.unsafeQueue"], + ["docBlame", "Aesop.Goal.unsafeQueue?"], + ["docBlame", "Aesop.Goal.unsafeRulesSelected"], + ["docBlame", "Aesop.Goal.withHeadlineTraceNode"], + ["docBlame", "Aesop.GoalData.addedInIteration"], + ["docBlame", "Aesop.GoalData.children"], + ["docBlame", "Aesop.GoalData.depth"], + ["docBlame", "Aesop.GoalData.failedRapps"], + ["docBlame", "Aesop.GoalData.id"], + ["docBlame", "Aesop.GoalData.isForcedUnprovable"], + ["docBlame", "Aesop.GoalData.isIrrelevant"], + ["docBlame", "Aesop.GoalData.lastExpandedInIteration"], + ["docBlame", "Aesop.GoalData.mvars"], + ["docBlame", "Aesop.GoalData.normalizationState"], + ["docBlame", "Aesop.GoalData.origin"], + ["docBlame", "Aesop.GoalData.parent"], + ["docBlame", "Aesop.GoalData.preNormGoal"], + ["docBlame", "Aesop.GoalData.state"], + ["docBlame", "Aesop.GoalData.successProbability"], + ["docBlame", "Aesop.GoalData.unsafeQueue"], + ["docBlame", "Aesop.GoalData.unsafeRulesSelected"], + ["docBlame", "Aesop.GoalDiff.check"], + ["docBlame", "Aesop.GoalDiff.checkCore"], + ["docBlame", "Aesop.GoalDiff.empty"], + ["docBlame", "Aesop.GoalId.dummy"], + ["docBlame", "Aesop.GoalId.one"], + ["docBlame", "Aesop.GoalId.succ"], + ["docBlame", "Aesop.GoalId.toNat"], + ["docBlame", "Aesop.GoalId.zero"], + ["docBlame", "Aesop.GoalOrigin.originalGoalId?"], + ["docBlame", "Aesop.GoalOrigin.toString"], + ["docBlame", "Aesop.GoalRef.checkAndMarkUnprovable"], + ["docBlame", "Aesop.GoalRef.extractSafePrefixScriptCore"], + ["docBlame", "Aesop.GoalRef.extractScriptCore"], + ["docBlame", "Aesop.GoalRef.free"], + ["docBlame", "Aesop.GoalRef.markForcedUnprovable"], + ["docBlame", "Aesop.GoalRef.markProvenByNormalization"], + ["docBlame", "Aesop.GoalRef.markSubtreeIrrelevant"], + ["docBlame", "Aesop.GoalRef.markUnprovable"], + ["docBlame", "Aesop.GoalState.isIrrelevant"], + ["docBlame", "Aesop.GoalState.isProven"], + ["docBlame", "Aesop.GoalState.isProvenByNormalization"], + ["docBlame", "Aesop.GoalState.isProvenByRuleApplication"], + ["docBlame", "Aesop.GoalState.isUnknown"], + ["docBlame", "Aesop.GoalState.isUnprovable"], + ["docBlame", "Aesop.GoalState.toEmoji"], + ["docBlame", "Aesop.GoalState.toNodeState"], + ["docBlame", "Aesop.GoalWithMVars.goal"], + ["docBlame", "Aesop.GoalWithMVars.mvars"], + ["docBlame", "Aesop.GoalWithMVars.ofMVarId"], + ["docBlame", "Aesop.HashSet.filter"], + ["docBlame", "Aesop.Index.add"], + ["docBlame", "Aesop.Index.applicableRules"], + ["docBlame", "Aesop.Index.byHyp"], + ["docBlame", "Aesop.Index.byTarget"], + ["docBlame", "Aesop.Index.fold"], + ["docBlame", "Aesop.Index.foldM"], + ["docBlame", "Aesop.Index.merge"], + ["docBlame", "Aesop.Index.trace"], + ["docBlame", "Aesop.Index.unindex"], + ["docBlame", "Aesop.Index.unindexed"], + ["docBlame", "Aesop.IndexMatchResult.locations"], + ["docBlame", "Aesop.IndexMatchResult.patternInstantiations"], + ["docBlame", "Aesop.IndexMatchResult.rule"], + ["docBlame", "Aesop.IndexingMode.format"], + ["docBlame", "Aesop.IndexingMode.hypsMatchingConst"], + ["docBlame", "Aesop.IndexingMode.targetMatchingConclusion"], + ["docBlame", "Aesop.Iteration.none"], + ["docBlame", "Aesop.Iteration.one"], + ["docBlame", "Aesop.Iteration.succ"], + ["docBlame", "Aesop.LIFOQueue.addGoals"], + ["docBlame", "Aesop.LIFOQueue.goals"], + ["docBlame", "Aesop.LIFOQueue.init"], + ["docBlame", "Aesop.LIFOQueue.popGoal"], + ["docBlame", "Aesop.LocalNormSimpRule.id"], + ["docBlame", "Aesop.LocalNormSimpRule.name"], + ["docBlame", "Aesop.LocalNormSimpRule.simpTheorem"], + ["docBlame", "Aesop.LocalRuleSet.add"], + ["docBlame", "Aesop.LocalRuleSet.applicableNormalizationRules"], + ["docBlame", "Aesop.LocalRuleSet.applicableNormalizationRulesWith"], + ["docBlame", "Aesop.LocalRuleSet.applicableSafeRules"], + ["docBlame", "Aesop.LocalRuleSet.applicableSafeRulesWith"], + ["docBlame", "Aesop.LocalRuleSet.applicableUnsafeRules"], + ["docBlame", "Aesop.LocalRuleSet.applicableUnsafeRulesWith"], + ["docBlame", "Aesop.LocalRuleSet.contains"], + ["docBlame", "Aesop.LocalRuleSet.containsGlobalSimpTheorem"], + ["docBlame", "Aesop.LocalRuleSet.empty"], + ["docBlame", "Aesop.LocalRuleSet.erase"], + ["docBlame", "Aesop.LocalRuleSet.modifyBase"], + ["docBlame", "Aesop.LocalRuleSet.modifyBaseM"], + ["docBlame", "Aesop.LocalRuleSet.onBase"], + ["docBlame", "Aesop.LocalRuleSet.onBaseM"], + ["docBlame", "Aesop.LocalRuleSet.trace"], + ["docBlame", "Aesop.LocalRuleSet.unindex"], + ["docBlame", "Aesop.LocalRuleSetMember.name"], + ["docBlame", "Aesop.LocalRuleSetMember.toGlobalRuleSetMember?"], + ["docBlame", "Aesop.MVarCluster.elim"], + ["docBlame", "Aesop.MVarCluster.goals"], + ["docBlame", "Aesop.MVarCluster.isIrrelevant"], + ["docBlame", "Aesop.MVarCluster.isIrrelevantNoCache"], + ["docBlame", "Aesop.MVarCluster.isProvenNoCache"], + ["docBlame", "Aesop.MVarCluster.isUnprovableNoCache"], + ["docBlame", "Aesop.MVarCluster.mk"], + ["docBlame", "Aesop.MVarCluster.modify"], + ["docBlame", "Aesop.MVarCluster.parent?"], + ["docBlame", "Aesop.MVarCluster.provenGoal?"], + ["docBlame", "Aesop.MVarCluster.setGoals"], + ["docBlame", "Aesop.MVarCluster.setIsIrrelevant"], + ["docBlame", "Aesop.MVarCluster.setParent"], + ["docBlame", "Aesop.MVarCluster.setState"], + ["docBlame", "Aesop.MVarCluster.state"], + ["docBlame", "Aesop.MVarCluster.stateNoCache"], + ["docBlame", "Aesop.MVarClusterData.goals"], + ["docBlame", "Aesop.MVarClusterData.isIrrelevant"], + ["docBlame", "Aesop.MVarClusterData.parent?"], + ["docBlame", "Aesop.MVarClusterData.state"], + ["docBlame", "Aesop.MVarClusterRef.checkAcyclic"], + ["docBlame", "Aesop.MVarClusterRef.checkConsistentParentChildLinks"], + ["docBlame", "Aesop.MVarClusterRef.checkIds"], + ["docBlame", "Aesop.MVarClusterRef.checkIntroducedMVars"], + ["docBlame", "Aesop.MVarClusterRef.checkInvariants"], + ["docBlame", "Aesop.MVarClusterRef.checkInvariantsIfEnabled"], + ["docBlame", "Aesop.MVarClusterRef.checkIrrelevance"], + ["docBlame", "Aesop.MVarClusterRef.checkMVars"], + ["docBlame", "Aesop.MVarClusterRef.checkState"], + ["docBlame", "Aesop.MVarClusterRef.extractSafePrefixScriptCore"], + ["docBlame", "Aesop.MVarClusterRef.extractScriptCore"], + ["docBlame", "Aesop.MVarClusterRef.free"], + ["docBlame", "Aesop.MVarClusterRef.markSubtreeIrrelevant"], + ["docBlame", "Aesop.MonadStats.readStatsRef"], + ["docBlame", "Aesop.Name.ofComponents"], + ["docBlame", "Aesop.Nanos.nanos"], + ["docBlame", "Aesop.Nanos.printAsMillis"], + ["docBlame", "Aesop.NodeState.isIrrelevant"], + ["docBlame", "Aesop.NodeState.isProven"], + ["docBlame", "Aesop.NodeState.isUnknown"], + ["docBlame", "Aesop.NodeState.isUnprovable"], + ["docBlame", "Aesop.NodeState.toEmoji"], + ["docBlame", "Aesop.NormM.Context"], + ["docBlame", "Aesop.NormRuleInfo.penalty"], + ["docBlame", "Aesop.NormRuleResult.newGoal?"], + ["docBlame", "Aesop.NormRuleResult.steps?"], + ["docBlame", "Aesop.NormRuleResult.toNormSeqResult"], + ["docBlame", "Aesop.NormSimpContext.configStx?"], + ["docBlame", "Aesop.NormSimpContext.enabled"], + ["docBlame", "Aesop.NormSimpContext.simprocs"], + ["docBlame", "Aesop.NormSimpContext.useHyps"], + ["docBlame", "Aesop.NormSimpRule.entries"], + ["docBlame", "Aesop.NormSimpRule.name"], + ["docBlame", "Aesop.NormStep.runPostSimpRules"], + ["docBlame", "Aesop.NormStep.runPreSimpRules"], + ["docBlame", "Aesop.NormStep.simp"], + ["docBlame", "Aesop.NormStep.unfold"], + ["docBlame", "Aesop.NormalizationState.isNormal"], + ["docBlame", "Aesop.NormalizationState.isProvenByNormalization"], + ["docBlame", "Aesop.NormalizationState.normalizedGoal?"], + ["docBlame", "Aesop.Options.queue"], + ["docBlame", "Aesop.Options.toOptions'"], + ["docBlame", "Aesop.Options'.forwardMaxDepth?"], + ["docBlame", "Aesop.Options'.generateScript"], + ["docBlame", "Aesop.Percent.fifty"], + ["docBlame", "Aesop.Percent.hundred"], + ["docBlame", "Aesop.Percent.ofFloat"], + ["docBlame", "Aesop.Percent.toFloat"], + ["docBlame", "Aesop.Percent.toHumanString"], + ["docBlame", "Aesop.Percent.δ"], + ["docBlame", "Aesop.PersistentHashSet.toArray"], + ["docBlame", "Aesop.PersistentHashSet.toList"], + ["docBlame", "Aesop.PhaseSpec.getSimpPrio"], + ["docBlame", "Aesop.PhaseSpec.phase"], + ["docBlame", "Aesop.PhaseSpec.toRule"], + ["docBlame", "Aesop.PostponedSafeRule.output"], + ["docBlame", "Aesop.PostponedSafeRule.rule"], + ["docBlame", "Aesop.PostponedSafeRule.toUnsafeRule"], + ["docBlame", "Aesop.Queue.addGoals"], + ["docBlame", "Aesop.Queue.init"], + ["docBlame", "Aesop.Queue.init'"], + ["docBlame", "Aesop.Queue.popGoal"], + ["docBlame", "Aesop.Rapp.appliedRule"], + ["docBlame", "Aesop.Rapp.assignedMVars"], + ["docBlame", "Aesop.Rapp.children"], + ["docBlame", "Aesop.Rapp.depth"], + ["docBlame", "Aesop.Rapp.elim"], + ["docBlame", "Aesop.Rapp.foldSubgoalsM"], + ["docBlame", "Aesop.Rapp.forSubgoalsM"], + ["docBlame", "Aesop.Rapp.id"], + ["docBlame", "Aesop.Rapp.introducedMVars"], + ["docBlame", "Aesop.Rapp.introducesMVar"], + ["docBlame", "Aesop.Rapp.isIrrelevant"], + ["docBlame", "Aesop.Rapp.isIrrelevantNoCache"], + ["docBlame", "Aesop.Rapp.isProvenNoCache"], + ["docBlame", "Aesop.Rapp.isSafe"], + ["docBlame", "Aesop.Rapp.isUnprovableNoCache"], + ["docBlame", "Aesop.Rapp.metaState"], + ["docBlame", "Aesop.Rapp.mk"], + ["docBlame", "Aesop.Rapp.modify"], + ["docBlame", "Aesop.Rapp.originalSubgoals"], + ["docBlame", "Aesop.Rapp.parent"], + ["docBlame", "Aesop.Rapp.parentPostNormMetaState"], + ["docBlame", "Aesop.Rapp.runMetaM"], + ["docBlame", "Aesop.Rapp.runMetaM'"], + ["docBlame", "Aesop.Rapp.runMetaMInParentState"], + ["docBlame", "Aesop.Rapp.runMetaMInParentState'"], + ["docBlame", "Aesop.Rapp.runMetaMModifying"], + ["docBlame", "Aesop.Rapp.runMetaMModifyingParentState"], + ["docBlame", "Aesop.Rapp.scriptSteps?"], + ["docBlame", "Aesop.Rapp.setAppliedRule"], + ["docBlame", "Aesop.Rapp.setAssignedMVars"], + ["docBlame", "Aesop.Rapp.setChildren"], + ["docBlame", "Aesop.Rapp.setId"], + ["docBlame", "Aesop.Rapp.setIntroducedMVars"], + ["docBlame", "Aesop.Rapp.setIsIrrelevant"], + ["docBlame", "Aesop.Rapp.setMetaState"], + ["docBlame", "Aesop.Rapp.setOriginalSubgoals"], + ["docBlame", "Aesop.Rapp.setParent"], + ["docBlame", "Aesop.Rapp.setScriptSteps?"], + ["docBlame", "Aesop.Rapp.setState"], + ["docBlame", "Aesop.Rapp.setSuccessProbability"], + ["docBlame", "Aesop.Rapp.state"], + ["docBlame", "Aesop.Rapp.stateNoCache"], + ["docBlame", "Aesop.Rapp.subgoals"], + ["docBlame", "Aesop.Rapp.successProbability"], + ["docBlame", "Aesop.Rapp.traceMetadata"], + ["docBlame", "Aesop.Rapp.traceTree"], + ["docBlame", "Aesop.Rapp.traceTreeCore"], + ["docBlame", "Aesop.Rapp.withHeadlineTraceNode"], + ["docBlame", "Aesop.RappData.appliedRule"], + ["docBlame", "Aesop.RappData.assignedMVars"], + ["docBlame", "Aesop.RappData.children"], + ["docBlame", "Aesop.RappData.id"], + ["docBlame", "Aesop.RappData.introducedMVars"], + ["docBlame", "Aesop.RappData.isIrrelevant"], + ["docBlame", "Aesop.RappData.metaState"], + ["docBlame", "Aesop.RappData.originalSubgoals"], + ["docBlame", "Aesop.RappData.parent"], + ["docBlame", "Aesop.RappData.scriptSteps?"], + ["docBlame", "Aesop.RappData.state"], + ["docBlame", "Aesop.RappData.successProbability"], + ["docBlame", "Aesop.RappId.dummy"], + ["docBlame", "Aesop.RappId.one"], + ["docBlame", "Aesop.RappId.succ"], + ["docBlame", "Aesop.RappId.toNat"], + ["docBlame", "Aesop.RappId.zero"], + ["docBlame", "Aesop.RappRef.extractSafePrefixScriptCore"], + ["docBlame", "Aesop.RappRef.extractScriptCore"], + ["docBlame", "Aesop.RappRef.free"], + ["docBlame", "Aesop.RappRef.markProven"], + ["docBlame", "Aesop.RappRef.markSubtreeIrrelevant"], + ["docBlame", "Aesop.RappRef.runMetaMModifying"], + ["docBlame", "Aesop.RegularRule.indexingMode"], + ["docBlame", "Aesop.RegularRule.isSafe"], + ["docBlame", "Aesop.RegularRule.isUnsafe"], + ["docBlame", "Aesop.RegularRule.name"], + ["docBlame", "Aesop.RegularRule.successProbability"], + ["docBlame", "Aesop.RegularRule.tac"], + ["docBlame", "Aesop.RegularRule.withRule"], + ["docBlame", "Aesop.Rule.compareByName"], + ["docBlame", "Aesop.Rule.compareByPriority"], + ["docBlame", "Aesop.Rule.compareByPriorityThenName"], + ["docBlame", "Aesop.Rule.extra"], + ["docBlame", "Aesop.Rule.indexingMode"], + ["docBlame", "Aesop.Rule.map"], + ["docBlame", "Aesop.Rule.mapM"], + ["docBlame", "Aesop.Rule.name"], + ["docBlame", "Aesop.Rule.pattern?"], + ["docBlame", "Aesop.Rule.tac"], + ["docBlame", "Aesop.RuleApplication.check"], + ["docBlame", "Aesop.RuleApplication.goals"], + ["docBlame", "Aesop.RuleApplication.postState"], + ["docBlame", "Aesop.RuleApplication.scriptSteps?"], + ["docBlame", "Aesop.RuleApplication.successProbability?"], + ["docBlame", "Aesop.RuleBuilder.apply"], + ["docBlame", "Aesop.RuleBuilder.applyCore"], + ["docBlame", "Aesop.RuleBuilder.cases"], + ["docBlame", "Aesop.RuleBuilder.casesCore"], + ["docBlame", "Aesop.RuleBuilder.checkUnfoldableConst"], + ["docBlame", "Aesop.RuleBuilder.constructors"], + ["docBlame", "Aesop.RuleBuilder.constructorsCore"], + ["docBlame", "Aesop.RuleBuilder.default"], + ["docBlame", "Aesop.RuleBuilder.forward"], + ["docBlame", "Aesop.RuleBuilder.forwardCore"], + ["docBlame", "Aesop.RuleBuilder.getApplyIndexingMode"], + ["docBlame", "Aesop.RuleBuilder.getCasesIndexingMode"], + ["docBlame", "Aesop.RuleBuilder.getConstructorsIndexingMode"], + ["docBlame", "Aesop.RuleBuilder.getForwardIndexingMode"], + ["docBlame", "Aesop.RuleBuilder.getImmediatePremises"], + ["docBlame", "Aesop.RuleBuilder.hasConst"], + ["docBlame", "Aesop.RuleBuilder.mkCasesTarget"], + ["docBlame", "Aesop.RuleBuilder.simp"], + ["docBlame", "Aesop.RuleBuilder.simpCore"], + ["docBlame", "Aesop.RuleBuilder.tactic"], + ["docBlame", "Aesop.RuleBuilder.tacticCore"], + ["docBlame", "Aesop.RuleBuilder.tacticIMode"], + ["docBlame", "Aesop.RuleBuilder.unfold"], + ["docBlame", "Aesop.RuleBuilder.unfoldCore"], + ["docBlame", "Aesop.RuleBuilderInput.options"], + ["docBlame", "Aesop.RuleBuilderInput.phase"], + ["docBlame", "Aesop.RuleBuilderInput.phaseName"], + ["docBlame", "Aesop.RuleBuilderInput.term"], + ["docBlame", "Aesop.RuleBuilderOptions.applyIndexTransparency"], + ["docBlame", "Aesop.RuleBuilderOptions.applyTransparency"], + ["docBlame", "Aesop.RuleBuilderOptions.casesIndexTransparency"], + ["docBlame", "Aesop.RuleBuilderOptions.casesPatterns"], + ["docBlame", "Aesop.RuleBuilderOptions.casesPatterns?"], + ["docBlame", "Aesop.RuleBuilderOptions.casesTransparency"], + ["docBlame", "Aesop.RuleBuilderOptions.constructorsIndexTransparency"], + ["docBlame", "Aesop.RuleBuilderOptions.constructorsTransparency"], + ["docBlame", "Aesop.RuleBuilderOptions.default"], + ["docBlame", "Aesop.RuleBuilderOptions.forwardIndexTransparency"], + ["docBlame", "Aesop.RuleBuilderOptions.forwardTransparency"], + ["docBlame", "Aesop.RuleBuilderOptions.immediatePremises?"], + ["docBlame", "Aesop.RuleBuilderOptions.indexingMode?"], + ["docBlame", "Aesop.RuleBuilderOptions.pattern?"], + ["docBlame", "Aesop.RuleFilter.matches"], + ["docBlame", "Aesop.RuleFilter.matchesBuilder"], + ["docBlame", "Aesop.RuleFilter.matchesPhase"], + ["docBlame", "Aesop.RuleFilter.matchesSimpTheorem?"], + ["docBlame", "Aesop.RuleFilter.name"], + ["docBlame", "Aesop.RuleFilter.scope"], + ["docBlame", "Aesop.RuleName.builder"], + ["docBlame", "Aesop.RuleName.compare"], + ["docBlame", "Aesop.RuleName.hash"], + ["docBlame", "Aesop.RuleName.name"], + ["docBlame", "Aesop.RuleName.phase"], + ["docBlame", "Aesop.RuleName.quickCompare"], + ["docBlame", "Aesop.RuleName.scope"], + ["docBlame", "Aesop.RulePattern.elab"], + ["docBlame", "Aesop.RulePattern.getInstantiation"], + ["docBlame", "Aesop.RulePattern.open"], + ["docBlame", "Aesop.RulePattern.openRuleType"], + ["docBlame", "Aesop.RulePattern.specializeRule"], + ["docBlame", "Aesop.RulePatternInstantiation.toArray"], + ["docBlame", "Aesop.RuleResult.isSuccessful"], + ["docBlame", "Aesop.RuleResult.toEmoji"], + ["docBlame", "Aesop.RuleSetName.isReserved"], + ["docBlame", "Aesop.RuleSetNameFilter.all"], + ["docBlame", "Aesop.RuleSetNameFilter.matchedRuleSetNames"], + ["docBlame", "Aesop.RuleSetNameFilter.matches"], + ["docBlame", "Aesop.RuleSetNameFilter.matchesAll"], + ["docBlame", "Aesop.RuleSetNameFilter.ns"], + ["docBlame", "Aesop.RuleStats.elapsed"], + ["docBlame", "Aesop.RuleStats.rule"], + ["docBlame", "Aesop.RuleStats.successful"], + ["docBlame", "Aesop.RuleStatsTotals.compareByTotalElapsed"], + ["docBlame", "Aesop.RuleStatsTotals.empty"], + ["docBlame", "Aesop.RuleTac.apply"], + ["docBlame", "Aesop.RuleTac.applyConst"], + ["docBlame", "Aesop.RuleTac.applyConsts"], + ["docBlame", "Aesop.RuleTac.applyExpr"], + ["docBlame", "Aesop.RuleTac.applyExpr'"], + ["docBlame", "Aesop.RuleTac.applyForwardRule"], + ["docBlame", "Aesop.RuleTac.applyTerm"], + ["docBlame", "Aesop.RuleTac.assertForwardHyp"], + ["docBlame", "Aesop.RuleTac.cases"], + ["docBlame", "Aesop.RuleTac.forward"], + ["docBlame", "Aesop.RuleTac.forwardConst"], + ["docBlame", "Aesop.RuleTac.forwardExpr"], + ["docBlame", "Aesop.RuleTac.forwardTerm"], + ["docBlame", "Aesop.RuleTac.makeForwardHyps"], + ["docBlame", "Aesop.RuleTac.ofSingleRuleTac"], + ["docBlame", "Aesop.RuleTac.ofTacticSyntax"], + ["docBlame", "Aesop.RuleTac.ruleTac"], + ["docBlame", "Aesop.RuleTac.ruleTacImpl"], + ["docBlame", "Aesop.RuleTac.singleRuleTac"], + ["docBlame", "Aesop.RuleTac.singleRuleTacImpl"], + ["docBlame", "Aesop.RuleTac.tacGen"], + ["docBlame", "Aesop.RuleTac.tacGenImpl"], + ["docBlame", "Aesop.RuleTac.tacticM"], + ["docBlame", "Aesop.RuleTac.tacticMImpl"], + ["docBlame", "Aesop.RuleTacDescr.run"], + ["docBlame", "Aesop.RuleTacInput.goal"], + ["docBlame", "Aesop.RuleTacInput.indexMatchLocations"], + ["docBlame", "Aesop.RuleTacInput.mvars"], + ["docBlame", "Aesop.RuleTacInput.options"], + ["docBlame", "Aesop.RuleTacInput.patternInstantiations"], + ["docBlame", "Aesop.RuleTacOutput.applications"], + ["docBlame", "Aesop.SafeExpansionM.State"], + ["docBlame", "Aesop.SafeRuleInfo.penalty"], + ["docBlame", "Aesop.SafeRuleInfo.safety"], + ["docBlame", "Aesop.SafeRuleResult.isSuccessfulOrPostponed"], + ["docBlame", "Aesop.SafeRuleResult.toEmoji"], + ["docBlame", "Aesop.SafeRulesResult.toEmoji"], + ["docBlame", "Aesop.SaturateM.Context"], + ["docBlame", "Aesop.Script.DynStructureM"], + ["docBlame", "Aesop.Script.DynStructureResult"], + ["docBlame", "Aesop.Script.LazyStep"], + ["docBlame", "Aesop.Script.SScript"], + ["docBlame", "Aesop.Script.STactic"], + ["docBlame", "Aesop.Script.StaticStructureM"], + ["docBlame", "Aesop.Script.Step"], + ["docBlame", "Aesop.Script.StepTree"], + ["docBlame", "Aesop.Script.Tactic"], + ["docBlame", "Aesop.Script.TacticBuilder"], + ["docBlame", "Aesop.Script.TacticState"], + ["docBlame", "Aesop.Script.UScript"], + ["docBlame", "Aesop.Script.UTactic"], + ["docBlame", "Aesop.Script.findFirstStep?"], + ["docBlame", "Aesop.Script.isConsecutiveSequence"], + ["docBlame", "Aesop.Script.matchGoals"], + ["docBlame", "Aesop.Script.mkOnGoal"], + ["docBlame", "Aesop.Script.mkOneBasedNumLit"], + ["docBlame", "Aesop.Script.orderedUScriptToSScript"], + ["docBlame", "Aesop.Script.sortDedupArrays"], + ["docBlame", "Aesop.Script.structureDynamicCore"], + ["docBlame", "Aesop.Script.structureStaticCore"], + ["docBlame", "Aesop.Script.withUpdatedMVarIds"], + ["docBlame", "Aesop.ScriptGenerated.toString"], + ["docBlame", "Aesop.ScriptT.run"], + ["docBlame", "Aesop.SearchM.Context"], + ["docBlame", "Aesop.SearchM.State"], + ["docBlame", "Aesop.SearchM.run"], + ["docBlame", "Aesop.SearchM.run'"], + ["docBlame", "Aesop.SimpResult.newGoal?"], + ["docBlame", "Aesop.SimpResult.toNormRuleResult"], + ["docBlame", "Aesop.SimpTheorems.addSimpEntry"], + ["docBlame", "Aesop.SimpTheorems.containsDecl"], + ["docBlame", "Aesop.SimpTheorems.foldSimpEntries"], + ["docBlame", "Aesop.SimpTheorems.foldSimpEntriesM"], + ["docBlame", "Aesop.SimpTheorems.simpEntries"], + ["docBlame", "Aesop.SingleRuleTac.toRuleTac"], + ["docBlame", "Aesop.Stats.configParsing"], + ["docBlame", "Aesop.Stats.empty"], + ["docBlame", "Aesop.Stats.ruleSelection"], + ["docBlame", "Aesop.Stats.ruleSetConstruction"], + ["docBlame", "Aesop.Stats.ruleStats"], + ["docBlame", "Aesop.Stats.ruleStatsTotals"], + ["docBlame", "Aesop.Stats.script"], + ["docBlame", "Aesop.Stats.scriptGenerated"], + ["docBlame", "Aesop.Stats.search"], + ["docBlame", "Aesop.Stats.total"], + ["docBlame", "Aesop.Stats.trace"], + ["docBlame", "Aesop.StatsExtensionState.empty"], + ["docBlame", "Aesop.StatsExtensionState.toStatsArray"], + ["docBlame", "Aesop.StatsReport.default"], + ["docBlame", "Aesop.StatsReport.instToStringNanos"], + ["docBlame", "Aesop.StatsReport.scripts"], + ["docBlame", "Aesop.SyntaxMap.Key"], + ["docBlame", "Aesop.SyntaxMap.empty"], + ["docBlame", "Aesop.SyntaxMap.find?"], + ["docBlame", "Aesop.SyntaxMap.findStx?"], + ["docBlame", "Aesop.SyntaxMap.insert"], + ["docBlame", "Aesop.SyntaxMap.insertWith"], + ["docBlame", "Aesop.SyntaxMap.toPHashMap"], + ["docBlame", "Aesop.SyntaxRewrite.focusRenameI"], + ["docBlame", "Aesop.SyntaxRewrite.keys"], + ["docBlame", "Aesop.SyntaxRewrite.run"], + ["docBlame", "Aesop.SyntaxRewriteMap.insert"], + ["docBlame", "Aesop.TraceOption.debug"], + ["docBlame", "Aesop.TraceOption.extraction"], + ["docBlame", "Aesop.TraceOption.isEnabled"], + ["docBlame", "Aesop.TraceOption.option"], + ["docBlame", "Aesop.TraceOption.proof"], + ["docBlame", "Aesop.TraceOption.ruleSet"], + ["docBlame", "Aesop.TraceOption.stats"], + ["docBlame", "Aesop.TraceOption.steps"], + ["docBlame", "Aesop.TraceOption.traceClass"], + ["docBlame", "Aesop.TraceOption.tree"], + ["docBlame", "Aesop.TraceOption.withEnabled"], + ["docBlame", "Aesop.Tree.nextGoalId"], + ["docBlame", "Aesop.Tree.nextRappId"], + ["docBlame", "Aesop.Tree.numGoals"], + ["docBlame", "Aesop.Tree.numRapps"], + ["docBlame", "Aesop.Tree.root"], + ["docBlame", "Aesop.Tree.rootMetaState"], + ["docBlame", "Aesop.TreeM.Context"], + ["docBlame", "Aesop.TreeM.run'"], + ["docBlame", "Aesop.TreeRef.markSubtreeIrrelevant"], + ["docBlame", "Aesop.TreeSpec.Goal"], + ["docBlame", "Aesop.TreeSpec.MVarCluster"], + ["docBlame", "Aesop.TreeSpec.Rapp"], + ["docBlame", "Aesop.TreeSpec.elimGoal"], + ["docBlame", "Aesop.TreeSpec.elimMVarCluster"], + ["docBlame", "Aesop.TreeSpec.elimRapp"], + ["docBlame", "Aesop.TreeSpec.introGoal"], + ["docBlame", "Aesop.TreeSpec.introMVarCluster"], + ["docBlame", "Aesop.TreeSpec.introRapp"], + ["docBlame", "Aesop.UnfoldRule.decl"], + ["docBlame", "Aesop.UnfoldRule.name"], + ["docBlame", "Aesop.UnfoldRule.unfoldThm?"], + ["docBlame", "Aesop.UnionFind.add"], + ["docBlame", "Aesop.UnionFind.addArray"], + ["docBlame", "Aesop.UnionFind.find?"], + ["docBlame", "Aesop.UnionFind.merge"], + ["docBlame", "Aesop.UnionFind.ofArray"], + ["docBlame", "Aesop.UnionFind.parents"], + ["docBlame", "Aesop.UnionFind.sets"], + ["docBlame", "Aesop.UnionFind.size"], + ["docBlame", "Aesop.UnionFind.sizes"], + ["docBlame", "Aesop.UnionFind.toRep"], + ["docBlame", "Aesop.UnorderedArraySet.ofHashSet"], + ["docBlame", "Aesop.UnorderedArraySet.ofPersistentHashSet"], + ["docBlame", "Aesop.UnorderedArraySet.partition"], + ["docBlame", "Aesop.UnorderedArraySet.toArray"], + ["docBlame", "Aesop.UnsafeQueue.entriesToMessageData"], + ["docBlame", "Aesop.UnsafeQueue.initial"], + ["docBlame", "Aesop.UnsafeQueueEntry.name"], + ["docBlame", "Aesop.UnsafeQueueEntry.successProbability"], + ["docBlame", "Aesop.UnsafeRuleInfo.successProbability"], + ["docBlame", "Aesop.addTryThisTacticSeqSuggestion.dedent"], + ["docBlame", "Aesop.aesop.smallErrorMessages"], + ["docBlame", "Aesop.applyS.tacticBuilder"], + ["docBlame", "Aesop.assertHypothesisS.tacticBuilder"], + ["docBlame", "Aesop.clearS.tacticBuilder"], + ["docBlame", "Aesop.elabPattern.adjustCtx"], + ["docBlame", "Aesop.expandGoal.doUnsafe"], + ["docBlame", "Aesop.expandGoal.fmtNorm"], + ["docBlame", "Aesop.expandGoal.fmtSafe"], + ["docBlame", "Aesop.expandGoal.fmtUnsafe"], + ["docBlame", "Aesop.expandNextGoal.fmt"], + ["docBlame", "Aesop.expandNextGoal.traceNewRapps"], + ["docBlame", "Aesop.getAppUpToDefeq.go"], + ["docBlame", "Aesop.getUnusedNames.dummyLDecl"], + ["docBlame", "Aesop.getUnusedNames.go"], + ["docBlame", "Aesop.hasSorry.go"], + ["docBlame", "Aesop.introsS.tacticBuilder"], + ["docBlame", "Aesop.introsUnfolding.run"], + ["docBlame", "Aesop.introsUnfoldingS.tacticBuilder"], + ["docBlame", "Aesop.normSimpCore.addLocalRules"], + ["docBlame", "Aesop.optimizeSyntaxWith.go"], + ["docBlame", "Aesop.optimizeSyntaxWith.optimizeHead"], + ["docBlame", "Aesop.renameInaccessibleFVarsS.tacticBuilder"], + ["docBlame", "Aesop.replaceFVarS.tacticBuilder"], + ["docBlame", "Aesop.runFirstUnsafeRule.loop"], + ["docBlame", "Aesop.runNormRuleTac.err"], + ["docBlame", "Aesop.saturateCore.go"], + ["docBlame", "Aesop.saturateCore.runFirstRule"], + ["docBlame", "Aesop.saturateCore.runRule"], + ["docBlame", "Aesop.splitFirstHypothesisS?.tacticBuilder"], + ["docBlame", "Aesop.splitTargetS?.tacticBuilder"], + ["docBlame", "Aesop.straightLineExt.go"], + ["docBlame", "Aesop.straightLineExtS.tacticBuilder"], + ["docBlame", "Aesop.tryCasesS.getUnusedCtorNames"], + ["docBlame", "Aesop.tryClearManyS.tacticBuilder"], + ["docBlame", "Aesop.tryClearS.tacticBuilder"], + ["docBlame", "Aesop.unfoldManyCore.pre"], + ["docBlame", "Aesop.withNormTraceNode.fmt"], + ["docBlame", "Aesop.withRuleTraceNode.fmt"], + ["docBlame", "Aesop.BestFirstQueue.ActiveGoal.addedInIteration"], + ["docBlame", "Aesop.BestFirstQueue.ActiveGoal.goal"], + ["docBlame", "Aesop.BestFirstQueue.ActiveGoal.lastExpandedInIteration"], + ["docBlame", "Aesop.BestFirstQueue.ActiveGoal.le"], + ["docBlame", "Aesop.BestFirstQueue.ActiveGoal.ofGoalRef"], + ["docBlame", "Aesop.BestFirstQueue.ActiveGoal.priority"], + ["docBlame", "Aesop.BuiltinRules.SubstitutableEq.fvarId"], + ["docBlame", "Aesop.BuiltinRules.SubstitutableEq.symm"], + ["docBlame", "Aesop.BuiltinRules.assumption.tryHyp"], + ["docBlame", "Aesop.BuiltinRules.destructProductsCore.go"], + ["docBlame", "Aesop.Check.script.steps"], + ["docBlame", "Aesop.ElabM.Context.forAdditionalGlobalRules"], + ["docBlame", "Aesop.ElabM.Context.forAdditionalRules"], + ["docBlame", "Aesop.ElabM.Context.forErasing"], + ["docBlame", "Aesop.ElabM.Context.forGlobalErasing"], + ["docBlame", "Aesop.ElabM.Context.goal"], + ["docBlame", "Aesop.ElabM.Context.parsePriorities"], + ["docBlame", "Aesop.EqualUpToIds.GoalContext.equalFVarIds"], + ["docBlame", "Aesop.EqualUpToIds.GoalContext.lctx₁"], + ["docBlame", "Aesop.EqualUpToIds.GoalContext.lctx₂"], + ["docBlame", "Aesop.EqualUpToIds.GoalContext.localInstances₁"], + ["docBlame", "Aesop.EqualUpToIds.GoalContext.localInstances₂"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore'"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore'"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.localContextsEqualUpToIdsCore"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.localDeclsEqualUpToIdsCore"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.unassignedMVarsEqualUpToIdsCore"], + ["docBlame", "Aesop.EqualUpToIdsM.Context.commonMCtx?"], + ["docBlame", "Aesop.EqualUpToIdsM.Context.mctx₁"], + ["docBlame", "Aesop.EqualUpToIdsM.Context.mctx₂"], + ["docBlame", "Aesop.EqualUpToIdsM.State.equalLMVarIds"], + ["docBlame", "Aesop.EqualUpToIdsM.State.equalMVarIds"], + ["docBlame", "Aesop.ExtractScriptM.Context.completeProof"], + ["docBlame", "Aesop.ExtractScriptM.State.script"], + ["docBlame", "Aesop.Frontend.AttrConfig.elab"], + ["docBlame", "Aesop.Frontend.AttrConfig.rules"], + ["docBlame", "Aesop.Frontend.BuilderOption.elab"], + ["docBlame", "Aesop.Frontend.CasesPattern.elab"], + ["docBlame", "Aesop.Frontend.DBuilderName.elab"], + ["docBlame", "Aesop.Frontend.DBuilderName.toBuilderName?"], + ["docBlame", "Aesop.Frontend.DBuilderName.toRuleBuilder"], + ["docBlame", "Aesop.Frontend.Feature.elab"], + ["docBlame", "Aesop.Frontend.IndexingMode.elab"], + ["docBlame", "Aesop.Frontend.Parser.additionalRule"], + ["docBlame", "Aesop.Frontend.Parser.additionalRules"], + ["docBlame", "Aesop.Frontend.Parser.aesop"], + ["docBlame", "Aesop.Frontend.Parser.«attr_rules[_]»"], + ["docBlame", "Aesop.Frontend.Parser.attr_rules_"], + ["docBlame", "Aesop.Frontend.Parser.bool_litFalse"], + ["docBlame", "Aesop.Frontend.Parser.bool_litTrue"], + ["docBlame", "Aesop.Frontend.Parser.builder_nameApply"], + ["docBlame", "Aesop.Frontend.Parser.builder_nameCases"], + ["docBlame", "Aesop.Frontend.Parser.builder_nameConstructors"], + ["docBlame", "Aesop.Frontend.Parser.builder_nameDefault"], + ["docBlame", "Aesop.Frontend.Parser.builder_nameDestruct"], + ["docBlame", "Aesop.Frontend.Parser.builder_nameForward"], + ["docBlame", "Aesop.Frontend.Parser.builder_nameSimp"], + ["docBlame", "Aesop.Frontend.Parser.builder_nameTactic"], + ["docBlame", "Aesop.Frontend.Parser.builder_nameUnfold"], + ["docBlame", "Aesop.Frontend.Parser.«builder_option(Cases_patterns:=[_])»"], + ["docBlame", "Aesop.Frontend.Parser.«builder_option(Immediate:=[_])»"], + ["docBlame", "Aesop.Frontend.Parser.«builder_option(Index:=[_])»"], + ["docBlame", "Aesop.Frontend.Parser.«builder_option(Pattern:=_)»"], + ["docBlame", "Aesop.Frontend.Parser.«builder_option(Transparency!:=_)»"], + ["docBlame", "Aesop.Frontend.Parser.«builder_option(Transparency:=_)»"], + ["docBlame", "Aesop.Frontend.Parser.«command#aesop_rules»"], + ["docBlame", "Aesop.Frontend.Parser.«command#aesop_stats_»"], + ["docBlame", "Aesop.Frontend.Parser.«commandErase_aesop_rules[_,,]»"], + ["docBlame", "Aesop.Frontend.Parser.command_Add_aesop_rules_"], + ["docBlame", "Aesop.Frontend.Parser.declareAesopRuleSets"], + ["docBlame", "Aesop.Frontend.Parser.elabDeclareAesopRuleSets"], + ["docBlame", "Aesop.Frontend.Parser.evalStatsReport?"], + ["docBlame", "Aesop.Frontend.Parser.featIdent"], + ["docBlame", "Aesop.Frontend.Parser.«feature(_)»"], + ["docBlame", "Aesop.Frontend.Parser.feature_"], + ["docBlame", "Aesop.Frontend.Parser.feature__1"], + ["docBlame", "Aesop.Frontend.Parser.feature__2"], + ["docBlame", "Aesop.Frontend.Parser.feature__3"], + ["docBlame", "Aesop.Frontend.Parser.feature__4"], + ["docBlame", "Aesop.Frontend.Parser.indexing_modeHyp_"], + ["docBlame", "Aesop.Frontend.Parser.indexing_modeTarget_"], + ["docBlame", "Aesop.Frontend.Parser.indexing_modeUnindexed"], + ["docBlame", "Aesop.Frontend.Parser.phaseNorm"], + ["docBlame", "Aesop.Frontend.Parser.phaseSafe"], + ["docBlame", "Aesop.Frontend.Parser.phaseUnsafe"], + ["docBlame", "Aesop.Frontend.Parser.«priority-_»"], + ["docBlame", "Aesop.Frontend.Parser.«priority_%»"], + ["docBlame", "Aesop.Frontend.Parser.ruleSetSpec"], + ["docBlame", "Aesop.Frontend.Parser.ruleSetsFeature"], + ["docBlame", "Aesop.Frontend.Parser.rule_expr_"], + ["docBlame", "Aesop.Frontend.Parser.«rule_expr_[_]»"], + ["docBlame", "Aesop.Frontend.Parser.rule_expr___"], + ["docBlame", "Aesop.Frontend.Parser.«tactic_clause(Add_)»"], + ["docBlame", "Aesop.Frontend.Parser.«tactic_clause(Config:=_)»"], + ["docBlame", "Aesop.Frontend.Parser.«tactic_clause(Erase_)»"], + ["docBlame", "Aesop.Frontend.Parser.«tactic_clause(Rule_sets:=[_])»"], + ["docBlame", "Aesop.Frontend.Parser.«tactic_clause(Simp_config:=_)»"], + ["docBlame", "Aesop.Frontend.Parser.transparency"], + ["docBlame", "Aesop.Frontend.Parser.usingRuleSets"], + ["docBlame", "Aesop.Frontend.PhaseName.elab"], + ["docBlame", "Aesop.Frontend.Priority.elab"], + ["docBlame", "Aesop.Frontend.Priority.toInt?"], + ["docBlame", "Aesop.Frontend.Priority.toPercent?"], + ["docBlame", "Aesop.Frontend.RuleConfig.addFeature"], + ["docBlame", "Aesop.Frontend.RuleConfig.buildGlobalRule"], + ["docBlame", "Aesop.Frontend.RuleConfig.buildLocalRule"], + ["docBlame", "Aesop.Frontend.RuleConfig.buildRule"], + ["docBlame", "Aesop.Frontend.RuleConfig.builder?"], + ["docBlame", "Aesop.Frontend.RuleConfig.builderOptions"], + ["docBlame", "Aesop.Frontend.RuleConfig.getBuilder"], + ["docBlame", "Aesop.Frontend.RuleConfig.getPenalty"], + ["docBlame", "Aesop.Frontend.RuleConfig.getPhase"], + ["docBlame", "Aesop.Frontend.RuleConfig.getPhaseSpec"], + ["docBlame", "Aesop.Frontend.RuleConfig.getRuleBuilderInput"], + ["docBlame", "Aesop.Frontend.RuleConfig.getSimpPriority"], + ["docBlame", "Aesop.Frontend.RuleConfig.getSuccessProbability"], + ["docBlame", "Aesop.Frontend.RuleConfig.getTerm"], + ["docBlame", "Aesop.Frontend.RuleConfig.phase?"], + ["docBlame", "Aesop.Frontend.RuleConfig.priority?"], + ["docBlame", "Aesop.Frontend.RuleConfig.ruleSets"], + ["docBlame", "Aesop.Frontend.RuleConfig.term?"], + ["docBlame", "Aesop.Frontend.RuleConfig.toRuleFilter"], + ["docBlame", "Aesop.Frontend.RuleConfig.validateForAdditionalRules"], + ["docBlame", "Aesop.Frontend.RuleExpr.buildAdditionalGlobalRules"], + ["docBlame", "Aesop.Frontend.RuleExpr.buildAdditionalLocalRules"], + ["docBlame", "Aesop.Frontend.RuleExpr.elab"], + ["docBlame", "Aesop.Frontend.RuleExpr.foldBranchesM"], + ["docBlame", "Aesop.Frontend.RuleExpr.toAdditionalGlobalRules"], + ["docBlame", "Aesop.Frontend.RuleExpr.toAdditionalLocalRules"], + ["docBlame", "Aesop.Frontend.RuleExpr.toAdditionalRules"], + ["docBlame", "Aesop.Frontend.RuleExpr.toGlobalRuleFilters"], + ["docBlame", "Aesop.Frontend.RuleExpr.toLocalRuleFilters"], + ["docBlame", "Aesop.Frontend.RuleExpr.toRuleConfigs"], + ["docBlame", "Aesop.Frontend.RuleExpr.toRuleFilters"], + ["docBlame", "Aesop.Frontend.RuleSetName.elab"], + ["docBlame", "Aesop.Frontend.RuleSets.elab"], + ["docBlame", "Aesop.Frontend.RuleSets.ruleSets"], + ["docBlame", "Aesop.Frontend.TacticConfig.additionalRules"], + ["docBlame", "Aesop.Frontend.TacticConfig.enabledRuleSets"], + ["docBlame", "Aesop.Frontend.TacticConfig.erasedRules"], + ["docBlame", "Aesop.Frontend.TacticConfig.getRuleSet"], + ["docBlame", "Aesop.Frontend.TacticConfig.options"], + ["docBlame", "Aesop.Frontend.TacticConfig.parse"], + ["docBlame", "Aesop.Frontend.TacticConfig.simpConfig"], + ["docBlame", "Aesop.Frontend.TacticConfig.simpConfigSyntax?"], + ["docBlame", "Aesop.Frontend.TacticConfig.updateRuleSet"], + ["docBlame", "Aesop.Frontend.elabSingleIndexingMode.elabKeys"], + ["docBlame", "Aesop.Frontend.eraseGlobalRules.go"], + ["docBlame", "Aesop.Goal.traceMetadata.trc"], + ["docBlame", "Aesop.Goal.traceMetadata.trcNode"], + ["docBlame", "Aesop.Goal.withHeadlineTraceNode.fmt"], + ["docBlame", "Aesop.GoalDiff.checkCore.isDefeqLocalDecl"], + ["docBlame", "Aesop.Index.applicableRules.insertIndexMatchResults"], + ["docBlame", "Aesop.Index.trace.traceArray"], + ["docBlame", "Aesop.Index.unindex.filterDiscrTree'"], + ["docBlame", "Aesop.LocalRuleSet.trace.printSimpSetName"], + ["docBlame", "Aesop.MVarClusterRef.checkAcyclic.go"], + ["docBlame", "Aesop.MVarClusterRef.checkConsistentParentChildLinks.err"], + ["docBlame", "Aesop.MVarClusterRef.checkIrrelevance.go"], + ["docBlame", "Aesop.MVarClusterRef.checkMVars.checkAssignedMVars"], + ["docBlame", "Aesop.MVarClusterRef.checkMVars.checkDroppedMVars"], + ["docBlame", "Aesop.MVarClusterRef.checkMVars.checkGoalMVars"], + ["docBlame", "Aesop.MVarClusterRef.checkMVars.checkNormMVars"], + ["docBlame", "Aesop.MVarClusterRef.checkMVars.getParentInfo"], + ["docBlame", "Aesop.MVarClusterRef.checkState.go"], + ["docBlame", "Aesop.NormM.Context.normSimpContext"], + ["docBlame", "Aesop.NormM.Context.options"], + ["docBlame", "Aesop.NormM.Context.ruleSet"], + ["docBlame", "Aesop.NormM.Context.statsRef"], + ["docBlame", "Aesop.Rapp.traceMetadata.trc"], + ["docBlame", "Aesop.RuleBuilder.default.err"], + ["docBlame", "Aesop.RuleBuilder.getImmediatePremises.errPrefix"], + ["docBlame", "Aesop.RuleBuilder.getImmediatePremises.isPatternInstantiated"], + ["docBlame", "Aesop.RulePattern.elab.abstractMVars'"], + ["docBlame", "Aesop.RulePattern.elab.fvarsToMVars"], + ["docBlame", "Aesop.RulePattern.elab.setMVarUserNamesToUniqueNames"], + ["docBlame", "Aesop.RuleTac.applyForwardRule.err"], + ["docBlame", "Aesop.RuleTac.assertForwardHyp.tacticBuilder"], + ["docBlame", "Aesop.RuleTac.cases.findFirstApplicableHyp"], + ["docBlame", "Aesop.RuleTac.cases.go"], + ["docBlame", "Aesop.RuleTac.makeForwardHyps.loop"], + ["docBlame", "Aesop.SafeExpansionM.State.numRapps"], + ["docBlame", "Aesop.SaturateM.Context.options"], + ["docBlame", "Aesop.Script.DynStructureM.Context"], + ["docBlame", "Aesop.Script.DynStructureM.State"], + ["docBlame", "Aesop.Script.DynStructureM.run"], + ["docBlame", "Aesop.Script.DynStructureResult.postState"], + ["docBlame", "Aesop.Script.DynStructureResult.script"], + ["docBlame", "Aesop.Script.LazyStep.BuildInput"], + ["docBlame", "Aesop.Script.LazyStep.build"], + ["docBlame", "Aesop.Script.LazyStep.erasePostStateAssignments"], + ["docBlame", "Aesop.Script.LazyStep.postGoals"], + ["docBlame", "Aesop.Script.LazyStep.postState"], + ["docBlame", "Aesop.Script.LazyStep.preGoal"], + ["docBlame", "Aesop.Script.LazyStep.preState"], + ["docBlame", "Aesop.Script.LazyStep.runFirstSuccessfulTacticBuilder"], + ["docBlame", "Aesop.Script.LazyStep.toStep"], + ["docBlame", "Aesop.Script.SScript.render"], + ["docBlame", "Aesop.Script.SScript.takeNConsecutiveFocusAndSolve?"], + ["docBlame", "Aesop.Script.STactic.numSubgoals"], + ["docBlame", "Aesop.Script.STactic.run"], + ["docBlame", "Aesop.Script.StaticStructureM.Context"], + ["docBlame", "Aesop.Script.StaticStructureM.State"], + ["docBlame", "Aesop.Script.StaticStructureM.run"], + ["docBlame", "Aesop.Script.Step.mkSorry"], + ["docBlame", "Aesop.Script.Step.postGoals"], + ["docBlame", "Aesop.Script.Step.postState"], + ["docBlame", "Aesop.Script.Step.preGoal"], + ["docBlame", "Aesop.Script.Step.preState"], + ["docBlame", "Aesop.Script.Step.render"], + ["docBlame", "Aesop.Script.Step.sTactic?"], + ["docBlame", "Aesop.Script.Step.tactic"], + ["docBlame", "Aesop.Script.Step.uTactic"], + ["docBlame", "Aesop.Script.Step.validate"], + ["docBlame", "Aesop.Script.StepTree.focusableGoals"], + ["docBlame", "Aesop.Script.StepTree.numSiblings"], + ["docBlame", "Aesop.Script.StepTree.toMessageData"], + ["docBlame", "Aesop.Script.StepTree.toMessageData?"], + ["docBlame", "Aesop.Script.Tactic.sTactic?"], + ["docBlame", "Aesop.Script.Tactic.skip"], + ["docBlame", "Aesop.Script.Tactic.structured"], + ["docBlame", "Aesop.Script.Tactic.uTactic"], + ["docBlame", "Aesop.Script.Tactic.unstructured"], + ["docBlame", "Aesop.Script.TacticBuilder.apply"], + ["docBlame", "Aesop.Script.TacticBuilder.applyStx"], + ["docBlame", "Aesop.Script.TacticBuilder.assertHypothesis"], + ["docBlame", "Aesop.Script.TacticBuilder.cases"], + ["docBlame", "Aesop.Script.TacticBuilder.casesOrObtain"], + ["docBlame", "Aesop.Script.TacticBuilder.clear"], + ["docBlame", "Aesop.Script.TacticBuilder.exactFVar"], + ["docBlame", "Aesop.Script.TacticBuilder.extN"], + ["docBlame", "Aesop.Script.TacticBuilder.intros"], + ["docBlame", "Aesop.Script.TacticBuilder.obtain"], + ["docBlame", "Aesop.Script.TacticBuilder.renameInaccessibleFVars"], + ["docBlame", "Aesop.Script.TacticBuilder.replace"], + ["docBlame", "Aesop.Script.TacticBuilder.simpAllOrSimpAtStarOnly"], + ["docBlame", "Aesop.Script.TacticBuilder.splitAt"], + ["docBlame", "Aesop.Script.TacticBuilder.splitTarget"], + ["docBlame", "Aesop.Script.TacticBuilder.substFVars"], + ["docBlame", "Aesop.Script.TacticBuilder.unfold"], + ["docBlame", "Aesop.Script.TacticBuilder.unfoldAt"], + ["docBlame", "Aesop.Script.TacticState.applyStep"], + ["docBlame", "Aesop.Script.TacticState.applyTactic"], + ["docBlame", "Aesop.Script.TacticState.eraseSolvedGoals"], + ["docBlame", "Aesop.Script.TacticState.focus"], + ["docBlame", "Aesop.Script.TacticState.getMainGoal?"], + ["docBlame", "Aesop.Script.TacticState.getVisibleGoalIndex"], + ["docBlame", "Aesop.Script.TacticState.getVisibleGoalIndex?"], + ["docBlame", "Aesop.Script.TacticState.invisibleGoals"], + ["docBlame", "Aesop.Script.TacticState.mkInitial"], + ["docBlame", "Aesop.Script.TacticState.onGoalM"], + ["docBlame", "Aesop.Script.TacticState.solveVisibleGoals"], + ["docBlame", "Aesop.Script.TacticState.visibleGoals"], + ["docBlame", "Aesop.Script.TacticState.visibleGoalsHaveMVars"], + ["docBlame", "Aesop.Script.UScript.checkIfEnabled"], + ["docBlame", "Aesop.Script.UScript.optimize"], + ["docBlame", "Aesop.Script.UScript.render"], + ["docBlame", "Aesop.Script.UScript.renderTacticSeq"], + ["docBlame", "Aesop.Script.UScript.toSScriptDynamic"], + ["docBlame", "Aesop.Script.UScript.toSScriptStatic"], + ["docBlame", "Aesop.Script.UScript.toStepTree"], + ["docBlame", "Aesop.Script.UScript.validate"], + ["docBlame", "Aesop.Script.matchGoals.getProperGoals"], + ["docBlame", "Aesop.Script.orderedUScriptToSScript.go"], + ["docBlame", "Aesop.Script.structureDynamicCore.applyStepAndSolveRemaining"], + ["docBlame", "Aesop.Script.structureDynamicCore.go"], + ["docBlame", "Aesop.Script.structureDynamicCore.goStructured"], + ["docBlame", "Aesop.Script.structureDynamicCore.goUnstructured"], + ["docBlame", "Aesop.Script.structureStaticCore.go"], + ["docBlame", "Aesop.Script.structureStaticCore.nextStep"], + ["docBlame", "Aesop.ScriptGenerated.toString.go"], + ["docBlame", "Aesop.SearchM.Context.normSimpContext"], + ["docBlame", "Aesop.SearchM.Context.options"], + ["docBlame", "Aesop.SearchM.Context.ruleSet"], + ["docBlame", "Aesop.SearchM.Context.statsRef"], + ["docBlame", "Aesop.SearchM.State.iteration"], + ["docBlame", "Aesop.SearchM.State.maxRuleApplicationDepthReached"], + ["docBlame", "Aesop.SearchM.State.queue"], + ["docBlame", "Aesop.SimpTheorems.foldSimpEntriesM.processTheorem"], + ["docBlame", "Aesop.StatsReport.default.fmtRuleStats"], + ["docBlame", "Aesop.SyntaxMap.Key.ofSyntax"], + ["docBlame", "Aesop.TreeM.Context.currentIteration"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore.instMVars"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore.printExpr"], + ["docBlame", + "Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore'.compareMVarValues"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore'.normalizeMVar"], + ["docBlame", "Aesop.EqualUpToIds.Unsafe.localContextsEqualUpToIdsCore.go"], + ["docBlame", + "Aesop.Frontend.RuleConfig.validateForAdditionalRules.getPhaseAndPriority"], + ["docBlame", "Aesop.Frontend.RuleExpr.foldBranchesM.go"], + ["docBlame", "Aesop.Frontend.TacticConfig.parse.addClause"], + ["docBlame", "Aesop.Frontend.TacticConfig.parse.go"], + ["docBlame", "Aesop.Script.DynStructureM.State.perfect"], + ["docBlame", "Aesop.Script.LazyStep.BuildInput.postGoals"], + ["docBlame", "Aesop.Script.LazyStep.BuildInput.tac"], + ["docBlame", "Aesop.Script.LazyStep.BuildInput.tacticBuilder"], + ["docBlame", "Aesop.Script.SScript.render.go"], + ["docBlame", "Aesop.Script.SScript.render.renderSTactic?"], + ["docBlame", "Aesop.Script.StaticStructureM.Context.steps"], + ["docBlame", "Aesop.Script.StaticStructureM.State.perfect"], + ["docBlame", "Aesop.Script.Step.validate.fmtGoals"], + ["docBlame", "Aesop.Script.StepTree.focusableGoals.go"], + ["docBlame", "Aesop.Script.StepTree.numSiblings.go"], + ["docBlame", "Aesop.Script.TacticBuilder.extN.mkPat"], + ["docBlame", "Aesop.Script.TacticState.eraseSolvedGoals.mvarWasSolved"], + ["docBlame", "Aesop.Script.UScript.toStepTree.go"], + ["docBlame", "Lean.Parser.Category.Aesop.attr_rules"], + ["docBlame", "Lean.Parser.Category.Aesop.bool_lit"], + ["docBlame", "Lean.Parser.Category.Aesop.builder_name"], + ["docBlame", "Lean.Parser.Category.Aesop.builder_option"], + ["docBlame", "Lean.Parser.Category.Aesop.feature"], + ["docBlame", "Lean.Parser.Category.Aesop.indexing_mode"], + ["docBlame", "Lean.Parser.Category.Aesop.phase"], + ["docBlame", "Lean.Parser.Category.Aesop.priority"], + ["docBlame", "Lean.Parser.Category.Aesop.rule_expr"], + ["docBlame", "Lean.Parser.Category.Aesop.tactic_clause"], + ["unusedArguments", "Aesop.withExceptionTransform"], + ["unusedArguments", "Aesop.applyS.tacticBuilder"], + ["unusedArguments", "Aesop.assertHypothesisS.tacticBuilder"], + ["unusedArguments", "Aesop.clearS.tacticBuilder"], + ["unusedArguments", "Aesop.splitTargetS?.tacticBuilder"], + ["unusedArguments", "Aesop.tryClearS.tacticBuilder"], + ["unusedArguments", "Aesop.RuleTac.assertForwardHyp.tacticBuilder"]] \ No newline at end of file From d4c69615d0776a818ecbf66eb92ea584abf7fef9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 22 Aug 2024 18:16:47 +1000 Subject: [PATCH 3/3] update nolints --- scripts/nolints.json | 21 +++------------------ 1 file changed, 3 insertions(+), 18 deletions(-) diff --git a/scripts/nolints.json b/scripts/nolints.json index 0bdd0876..522c5b8f 100644 --- a/scripts/nolints.json +++ b/scripts/nolints.json @@ -90,9 +90,6 @@ ["docBlame", "Aesop.StatsExtensionState"], ["docBlame", "Aesop.StatsRef"], ["docBlame", "Aesop.StatsReport"], - ["docBlame", "Aesop.SyntaxMap"], - ["docBlame", "Aesop.SyntaxRewrite"], - ["docBlame", "Aesop.SyntaxRewriteMap"], ["docBlame", "Aesop.TraceOption"], ["docBlame", "Aesop.Tree"], ["docBlame", "Aesop.TreeM"], @@ -229,9 +226,10 @@ ["docBlame", "Aesop.normalizeGoalMVar"], ["docBlame", "Aesop.optNormRuleResultEmoji"], ["docBlame", "Aesop.optNormRuleResultToNormSeqResult"], + ["docBlame", "Aesop.optimizeFocusRenameI"], + ["docBlame", "Aesop.optimizeInitialRenameI"], ["docBlame", "Aesop.optimizeScript"], ["docBlame", "Aesop.optimizeSyntax"], - ["docBlame", "Aesop.optimizeSyntaxWith"], ["docBlame", "Aesop.popGoal?"], ["docBlame", "Aesop.postTraverseDown"], ["docBlame", "Aesop.postTraverseUp"], @@ -1023,17 +1021,6 @@ ["docBlame", "Aesop.StatsReport.default"], ["docBlame", "Aesop.StatsReport.instToStringNanos"], ["docBlame", "Aesop.StatsReport.scripts"], - ["docBlame", "Aesop.SyntaxMap.Key"], - ["docBlame", "Aesop.SyntaxMap.empty"], - ["docBlame", "Aesop.SyntaxMap.find?"], - ["docBlame", "Aesop.SyntaxMap.findStx?"], - ["docBlame", "Aesop.SyntaxMap.insert"], - ["docBlame", "Aesop.SyntaxMap.insertWith"], - ["docBlame", "Aesop.SyntaxMap.toPHashMap"], - ["docBlame", "Aesop.SyntaxRewrite.focusRenameI"], - ["docBlame", "Aesop.SyntaxRewrite.keys"], - ["docBlame", "Aesop.SyntaxRewrite.run"], - ["docBlame", "Aesop.SyntaxRewriteMap.insert"], ["docBlame", "Aesop.TraceOption.debug"], ["docBlame", "Aesop.TraceOption.extraction"], ["docBlame", "Aesop.TraceOption.isEnabled"], @@ -1105,8 +1092,7 @@ ["docBlame", "Aesop.introsUnfolding.run"], ["docBlame", "Aesop.introsUnfoldingS.tacticBuilder"], ["docBlame", "Aesop.normSimpCore.addLocalRules"], - ["docBlame", "Aesop.optimizeSyntaxWith.go"], - ["docBlame", "Aesop.optimizeSyntaxWith.optimizeHead"], + ["docBlame", "Aesop.optimizeInitialRenameI.tacsToTacticSeq"], ["docBlame", "Aesop.renameInaccessibleFVarsS.tacticBuilder"], ["docBlame", "Aesop.replaceFVarS.tacticBuilder"], ["docBlame", "Aesop.runFirstUnsafeRule.loop"], @@ -1406,7 +1392,6 @@ ["docBlame", "Aesop.SearchM.State.queue"], ["docBlame", "Aesop.SimpTheorems.foldSimpEntriesM.processTheorem"], ["docBlame", "Aesop.StatsReport.default.fmtRuleStats"], - ["docBlame", "Aesop.SyntaxMap.Key.ofSyntax"], ["docBlame", "Aesop.TreeM.Context.currentIteration"], ["docBlame", "Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore.instMVars"], ["docBlame", "Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore.printExpr"],