Linter false positive

Stream: lean4

[jthulhu]

The following code

inductive Foo {α : Type} : α → Type where
  | bar (x : α) : Foo x

def Foo.baz {α : Type} (x : α) : Foo x → Foo x
  | bar _ => bar _

triggers a warning: usused variable `x` , reported at the location of the wildcard pattern in the Foo.baz definition. This is presumably not the intended behavior, as x is used in the signature, and the lint is reported at the wrong place.

[Kim Morrison]

Could you please open an issue?

[jthulhu]

Done.