Goto definition for Lean.Elab in vscode

Stream: lean4

[Rikiya Kashiwagi]

VSCode's goto definition for Lean.Elab, such as "def" keyword or "→" symbol helps me so much explore the Lean's parser and macro system. However, some files can do that and some cannnot under the same settings. Do you have any ideas of the problem?

[Mario Carneiro]

You have to have the relevant files imported, meaning import Lean at the top of the file should do the trick

[Rikiya Kashiwagi]

Ah, I see. that's hard to figure out by myself.
Thanks!