Getting the InfoTree for a theorem

Stream: new members

[Olivier Bousquet]

Let's say I have defined and proved a theorem called my_theorem. What is the easiest way to programmatically get the InfoTree corresponding to its proof?

[Anand Rao Tadipatri]

The only way I know of is to first figure out the file where the declaration is contained, get the InfoTree of that file and then try to locate the declaration within, but someone might have a better way.

[Mario Carneiro]

There is currently no real support for this, if you are interested in theorems from files other than the current one. You would have to re-elaborate the relevant file from scratch (and doing this in the same process as an existing lean elaboration is somewhat hazardous due to the use of global variables in the elaborator), and watch for when the theorem of interest is added to the environment to deduce which command is relevant and has the info trees you want. Doable, but very expensive, and untested (there may be additional unforeseen issues that arise when attempting this).