Lean4
@[inherit_doc Mathlib.Linter.linter.style.multiGoal]
def multiGoalLinter : Linter where
run :=
withSetOptionIn fun _stx ↦ do
unless getLinterValue linter.style.multiGoal (← getLinterOptions) do
return
if (← get).messages.hasErrors then
return
let trees ← getInfoTrees
for t in trees do
for (s, before, after, n) in getManyGoals t do
let goals (k : Nat) := if k == 1 then f!"1 goal" else f! "{k} goals"
let fmt ←
Command.liftCoreM
try
PrettyPrinter.ppTactic ⟨s⟩
catch _ =>
pure f!"(failed to pretty print)"
Linter.logLint linter.style.multiGoal s
m!"\
The following tactic starts with {(goals before)} and ends with {(goals after)}, \
{n} of which {(if n == 1 then "is" else "are")} not operated on.\
{indentD fmt}\n\
Please focus on the current goal, for instance using `·` (typed as \"\\.\")."
