RFC: `recall` a `structure`

Proposal

Generalize the recall command to allow recalling a structure that was previously defined.

The recall command is underused but invaluable for publishing complicated formalization projects. Advanced math projects may have hundreds of definitions and thousands of lemmas but, in the end, there is perhaps one final theorem whose statement depends on just a few dozen of definitions. For future readers, it is important to be able to check what the final result is and whether the definitions used in it correspond to their intuition about what notions were formalized. For such purposes, it is great to include a "recap" section in the final file of the project, such as we do in the Seymour project:
https://github.com/Ivan-Sergeyev/seymour/blob/74640d8a57a6c95bc7e7007559554a1ec7835267/Seymour.lean
Ideally, such a "recap" section is formally verified, that is, mechanically checked that it accurately repeats the definitions and theorems from the project. This is exactly what the recall command does!

Unfortunately, the current recall command does not support structure declarations. As a result, we resort to workarounds such as the following:
https://github.com/Ivan-Sergeyev/seymour/blob/74640d8a57a6c95bc7e7007559554a1ec7835267/Seymour.lean#L32-L43
Note that the #guard_msgs part was necessary.

It would be much better to be able to write

recall inductive

and

recall structure

as @jcommelin suggested.

Community Feedback

Discussion:
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.60recall.60.20on.20.60structure.60

Start with the existing recall command and the linked Seymour.lean workaround, then read the linked Zulip discussion for design context. Done means the proposed recall structure and recall inductive forms can verify previously defined declarations without that workaround.