linter for double variable declarations

Stream: general

[Sebastien Gouezel]

Is it easy to have a linter for double declarations of the same variable? Like

variable {α : Type*}

at the top of the file, and 600 lines below the same

variable {α : Type*}

shadowing the first one?

[Bolton Bailey]

Seems tricky, it could be that the second one is actually just resetting the implicitness from a third variable (α : Type*) somewhere in the middle.

[Bolton Bailey]

Am I right about how that works? If I have variable {α : Type*} to start with, I can later do variable (α : Type*) if I want a section where it's explicit?

[Yaël Dillies]

No, you do variable (α) instead.

[Bolton Bailey]

Either way, seems reasonable, I've added it to the wishlist.

[Bolton Bailey]

Frankly, it would be good to have a linter that catches any variable shadowing of any form, ever, period.

[Patrick Massot]

There are legitimate uses of variable shadowing, especially when programming.

[Eric Wieser]

I'd argue that shadowing should only be allowed within a new section, like it is in C

[Bolton Bailey]

Patrick Massot said:

There are legitimate uses of variable shadowing, especially when programming.

Is there a particular example of such a legitimate use in mathlib that you could point out? I'd like to have a better sense of this.