unused anonymous argument

Stream: std4

[Patrick Massot]

Is the following linter error expected?

import Std.Tactic.Lint

/-- My foo function. -/
def foo (_ : Nat) := 0

#lint

The underscore makes it clear I want this to be an unused argument.

[Mario Carneiro]

It is expected, yes. The mathlib/std unused arguments linter looks at the underlying expression and doesn't care about argument names

[Patrick Massot]

Is this considered to be a bug or a feature?

[Mario Carneiro]

a behavior :shrug:

[James Gallicchio]

(unlike the core unused-arg linter, which fails to catch non-syntactic uses, right?)

[Mario Carneiro]

I can see uses for it

[Mario Carneiro]

right @James Gallicchio

[Mario Carneiro]

for instance you can use def foo (_ : Nat) : Nat := by assumption to make a non-constant function with an unnamed argument

[Mario Carneiro]

calling the variable x there would probably trigger the core linter

[Mario Carneiro]

the mathlib linter is more about actually detecting constant functions