generate defining equations of recursors

Stream: lean4

[Alexander Bentkamp]

Is there any (meta)code to generate the defining equations of recursors? So for example, for the Nat type, I'd like to generate the equations

Nat.rec a b Nat.zero = a
Nat.rec a b (Nat.succ c) = b c (Nat.rec a b c)

Of course, all of these are provable by rfl, but the tactic I am working on cannot deal with definitional equality.

[Jannis Limperg]

Not that I know of. Should be fairly easy to write though. (There may be problems with nested and mutual types; I don't even know whether we generate proper recursors for these.) I can give it a shot if you want.

[Alexander Bentkamp]

Ok, thanks, I'll try to implement it myself.

[Marcus Rossel]

(deleted)

[Mario Carneiro]

@Alexander Bentkamp The defining equations of recursors are actually stored in the RecursorVal for consumption by the kernel, see src#Lean.RecursorRule