Which theorems get automatically generated for inductives?

Stream: general

[Markus de Medeiros]

Hopefully this is a simple question, but I can't seem to find an answer by searching. When I declare something with inductive T := ... , which theorems (like T.rec, T.recOn) does Lean generate about T? More generally, is there a flag I can set to see the declarations Lean is making behind the scenes?

[Edward van de Meent]

i think there's a command along the lines of whatsnew in which shows this?

[Edward van de Meent]

it is only defined in mathlib afaict, tho

[Edward van de Meent]

fwiw, this seems like the kind of thing that can easily be upstreamed into batteries

[Markus de Medeiros]

This is exactly what I was looking for, thanks!

[Markus de Medeiros]

It might be nice to have this upstreamed, since I think this information is available "out of the box" in Rocq

[Edward van de Meent]

ikr?

[Kim Morrison]

I think it would be pretty reasonable to upstream it either to Batteries or to Lean. If someone wanted to do this I would review the PR! (And in the Lean case, I'm happy to assist converting the elab to a @[builtin_command_elab (e.g. Lean.Elab.Tactic.GuardMsgs.elabGuardMsgs is a good model to follow).)