Linting for bad instances

Stream: mathlib4

[Bhavik Mehta]

I just came across docs#Nat.Partition.decidableEqParition which is a decidable instance that can't reduce. I'm making a PR right now to fix it (and in Lean 3 this instance could be generated automatically, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deriving.20DecidableEq.20fails.20with.20implicit.20argument), but is it possible to automatically lint or check for such instances?

[Eric Wieser]

docs#Nat.Partition.decidableEqParition

[Eric Wieser]

Maybe it's time for a spelling linter too

[Bhavik Mehta]

Eric Wieser said:

docs#Nat.Partition.decidableEqParition

Oops, thanks, I'm still used to the mathlib3 docs search where it automatically figures this out! Edited.