Zulip Chat Archive

Stream: mathlib4

Topic: elab_as_elim


Scott Morrison (Nov 30 2022 at 00:04):

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 (Nov 30 2022 at 00:04):

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

Sebastian Ullrich (Nov 30 2022 at 09:39):

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 (Jan 23 2023 at 13:36):

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 (Jan 23 2023 at 13:38):

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


Last updated: Dec 20 2023 at 11:08 UTC