Eq.ndrec

Stream: metaprogramming / tactics

[Leni Aniva]

Why is Eq.ndrec not a recursor? Is it possible to construct a RecursorInfo corresponding to Eq.ndrec?

#eval do
  let rn ← Meta.mkRecursorInfo ``Eq.ndrec
  IO.println s!"{rn.majorPos}"

[Aaron Liu]

It's defined in terms of Eq.rec

[Aaron Liu]

I don't think you'll be able to write a RecursorInfo corresponding to Eq.ndrec that the kernel accepts misunderstood the question

[Kyle Miller]

(I think Leni's question is why is it not registered as a recursor. The casesOn definitions work, yet they're defined in terms of rec)

[Kyle Miller]

For unregistered recursors, at least you can specify the major position, like

Meta.mkRecursorInfo ``Eq.ndrec (some 5)

[Kyle Miller]

I guess someone could add recursor 5 to the attributes for Eq.ndrec, but it looks like there are no other uses of this attribute in all of core.

[Kyle Miller]

I don't know what you're up to, but you could consider unfolding Eq.ndrec first, since that exposes Eq.rec, which is already a recursor.