elab_as_elim

Stream: mathlib4

[Scott Morrison]

I'm getting an error on

@[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

saying unexpected eliminator resulting type P _x✝.1 _x✝.2.

Any ideas?

[Scott Morrison]

We have two of these in porting Data.Nat.Basic.

[Sebastian Ullrich]

I think it's trying to apply the attribute to the WF recursion helper? That sounds like a bug. Applying it afterwards works.

attribute [elab_as_elim] strongSubRecursion

[Xavier Roblot]

While searching for a solution to a similar bug with elab_as_elim, I noticed that the line

attribute [elab_as_elim] strongSubRecursion

that was added to Data.Nat.Basic has been copy-paste to use for pincerRecursion a few lines below but the name of the result was not changed, see mathlib4#1781 for a fix.

[Xavier Roblot]

BTW, applying the attribute afterwards does not fix the problem with elab_as_elim in my case, see mathlib4#1777