go to def for generated theorems

Stream: lean4

[Tomas Skrivan]

I have a custom command that adds a bunch of new theorems to the environment. Right now 'go to definition' does not work on these theorems. How can I make sure that it will take me to the command that generates them?

[Eric Wieser]

Likely you want to call docs#Lean.Elab.Term.addTermInfo

[Kyle Miller]

docs#Lean.Elab.addDeclarationRangesFromSyntax

TermInfo is more for making it so that hovering over an identifier shows the constant that was defined, and it's also used to support "go to definition", but only from within the same module. Declaration ranges work across modules.