The nolint on empty_relation is to avoid this error:

/- The `unusedArguments` linter reports:
UNUSED ARGUMENTS. -/
-- Mathlib.Init.Logic
#check empty_relation.{u} /- argument 2 x✝¹ : α, argument 3 x✝ : α -/

I suspect the linter has a bug.

I think the linter is correct, and the @[nolint] annotation is also correct. This definition actually does have unused arguments.

def empty_relation := λ _ _ : α => False

Yes, those _ arguments are unused, but shouldn't the linter ignore them because they are named _? In my editor I don't see them underlined by a warning squiggle -- it's only when I do runLinter that I get the error.

There are two kinds of linters here: the lean core linters, and the mathlib linters. The lean core linters are reported as you type and are controlled by set_option linter.*, and the mathlib linters are run when you call runLinter or in CI and are controlled by the nolints.txt file and the @[nolint] annotation.

The mathlib linters generally look at declarations in the environment, and are of a more "semantic" nature than the lean core linters that look at the syntax of what you wrote. The unusedArguments linter is a mathlib linter, and it doesn't care if you wrote a _ or not, it's trying to determine if you actually didn't use an argument after all the tactics have run to produce a term. You are thinking of the linter.unusedVariables lean core linter, which checks whether you have actually referred to a variable in the written syntax and honors _x variable naming.

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build