Unused variable in decreasing_by

Stream: lean4

[Marcus Rossel]

In the following example, h is marked as being unused even though it is used in the decreasing_by block:

def f (n : Nat) : Nat :=
  match h : n with
  | 0 => 0
  | m + 1 => f m
termination_by f n => n
decreasing_by
  simp_wf
  simp [h, Nat.lt_succ_self]

Is this expected behavior?

[Yaël Dillies]

You can usually avoid this by using * instead of h in the simp call

[Marcus Rossel]

But should h be marked as unused in the first place?

[Marcus Rossel]

And the only way to actually get the hypothesis into the context of the decreasing_by block is to name it. So I'd still have to call it _h to avoid the linter.

[Joachim Breitner]

Yeah, known issue (https://github.com/leanprover/lean4/issues/2920). Work arounds are underscores or locally disabling the linter