How do I get the infotree corresponding to a declaration?

Stream: lean4

[nrs]

Is there any function I can run in CoreM or MetaM that will get me the info tree of a declaration? Would this probably a function that takes a ConstantInfo?

[nrs]

seems like MonadInfoTree provides a method for this

[nrs]

hm,

run_meta do
  dbg_trace (<- Lean.Elab.MonadInfoTree.getInfoState).trees.size
  dbg_trace (<- Lean.Elab.getInfoTrees).size

are both printing 0 but I have three named declaration in the document, anyone know what might cause this?

[nrs]

ah using Lean.Elab.Command.CommandElabM (or run_cmd) instead works. anyone with knowledge of the internals that could explain this? edit: oh but it seems to only get infotrees related to the current declaration and doesn't grab the previous declarations)

[David Renshaw]

The only way I know of getting an InfoTree is to elaborate commands yourself. This can be done via Frontend.processCommand. If there's a more direct way, I'd be interested in hearing about it!

[nrs]

Thanks for the tip! Trying out stuff in the Elab.Frontend module

[Adam Topaz]

I have some helper functions for such things here: https://github.com/adamtopaz/lean_extras/blob/master/LeanExtras/Frontend.lean

[nrs]

woah very cool stuff! thanks a lot!