Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

@[elab_as_elim]
def strongSubRecursion {P : Nat → Nat → Sort _} (H : ∀ a b, (∀ x y, x < a → y < b → P x y) → P a b) :
    ∀ n m : Nat, P n m
  | n, m => H n m fun x y _ _ => strongSubRecursion H x y

fails with unexpected eliminator resulting type P _x✝.1 _x✝.2.

@Kha suggested on zulip that "I think it's trying to apply the attribute to the WF recursion helper?"

Applying the attribute afterwards is a satisfactory workaround for now.

Versions

Lean (version 4.0.0-nightly-2022-11-29, commit 5286c2b, Release)