Get current InfoTree

Stream: metaprogramming / tactics

[Jannis Limperg]

@moatez ouertatani and I are trying to write a linter (Lean.Linter) which makes some suggestions for optimising tactic proofs. These suggestions require elaboration information (e.g. the types of certain variables), and since the linter runs after the declaration has been elaborated, I thought we should be able to get access to the InfoTree nodes for the declaration and get the elab information from them. However, I couldn't immediately figure out how to get the relevant InfoTree(s). Any pointers?

[Jannis Limperg]

@moatez ouertatani It seems like the unused variable linter uses the same strategy, so you should be able to adapt its implementation. It retrieves the current InfoTrees here and processes them here.