linter unusedSectionVars false positive

Stream: lean4

[Xavier Roblot]

It was necessary in #27706 to disable linter.unusedSectionVars before docs#IsLocalization.AtPrime.equivQuotientMapMaximalIdeal_apply_mk, see this for the comment on why this is the case.

@Riccardo Brasca suggested that I ask here it if was something worth opening an issue.

[Notification Bot]

This topic was moved here from #mathlib4 > linter unusedSectionVars false positive by Riccardo Brasca.

[Aaron Liu]

is this the same as #lean4 > unused section variable linter is buggy @ 💬

[Kim Morrison]

That thread reports two problems, one involving where clauses, which has an open issue lean#11917, and another one that looks similar to this but doesn't have an open issue.

So opening on issue for this (perhaps including the example from the other thread, as that is already an #mwe) would be great.

[Kim Morrison]

(If you're feeling energetic you could run the mathlib-minimizer on this example. :-)