Linters

Stream: mathlib4

[Yury G. Kudryashov]

Do we no longer have a "Decidable that is not used in the type" linter? I just noticed that docs#MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top has an unneeded decidability assumption.

[Sébastien Gouëzel]

No, we don't have it. In fact most linters from mathlib3 are missing in mathlib4, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/List.20of.20linters/near/400483203. Most of them wouldn't probably be hard to implement by someone with enough meta skills, but time is precious for everyone.