Hypothesis marked as unused, bug?

Stream: new members

[Philogy]

I have the following recursive method with a proof of termination, relying on the match hypothesis h:

def consume' (input expected : String): Except String String :=
  match h: input.data, expected.data with
  | _, [] => .ok input
  |  i::rem_input, e::rem_expected =>
    if i == e
    then consume' ⟨rem_input⟩ ⟨rem_expected⟩
    else .error ⟨rem_input⟩
  | [], _ => .error ""
termination_by input.length
decreasing_by {
  have eq_rem_len_plus_one : rem_input.length + 1 = input.length := by
    simp [String.length, h]
  rw [← eq_rem_len_plus_one]
  exact Nat.lt_add_one rem_input.length
}

However the above code gives me a warning that h is unused even though it is necessary in the termination proof. Two questions:

1. Is this a bug?
2. Is there are alternative syntax where the termination proof is in the body of the function such that h is recognized to be used?

[Martin Dvořák]

[my bad]

[Martin Dvořák]

Yes, it looks like a bug to me.