how to disable unusedArguments linter (docs)

Stream: mathlib4

[Edward van de Meent]

on #34789, i ran into the following:
I was asked to disable the unusedArguments linter for a declaration. The linter warning itself didn't tell me what to do, so remembering that there's several options which disable certain linters, i tried set_option linter.unusedArguments false in which failed. Then, i searched mathlib for a set_option linter.unused* occurrence (which there isn't). I also at some point tried to find unusedArguments but failed (which in retrospect was probably caused by a typo of some sort). Finally, I asked and was told the correct incantation was @[nolint unusedArguments].

All this is to say, it'd be nice if the linter tells you that you can use @[nolint unusedArguments] to disable it for some declaration, so i don't have to look it up next time...

[Edward van de Meent]

also, it might be confusing that there's also the unusedVariables linter which does have an option one can toggle.

[Anne Baanen]

The distinction between environment linters (which use @[nolint]) and syntax linters (which use set_option) is quite annoying in general. I wonder how possible/hard it would be for environment linters to parse set_option statements...

[Floris van Doorn]

I agree that environment linters should tell how to disable themselves! PR welcome! (I believe that would be a PR to Batteries(?))
I don't think environment linters can deal with set_option statements. Whether an option was set during the elaboration of a particular declaration is not stored in the Environment...

[Bryan Gin-ge Chen]

Floris van Doorn said:

I agree that environment linters should tell how to disable themselves! PR welcome! (I believe that would be a PR to Batteries(?))

(See open issue batteries#1468)