Getting the current namespace in vscode

Stream: new members

[Eric Wieser]

When looking at a multi-thousand line mathlib file in vscode, it's sometimes quite hard to work out what namespace the lemma I'm looking at is in.

Is there an easy way to find out?

[Rob Lewis]

#where

[Eric Wieser]

Ah, but if I type that in my editor won't mathlib rebuild?

[Alex J. Best]

well as long as you close the file after and dont save (and maybe restart lean) it should be fine

[Alex J. Best]

An alternative is to look at the declarations you want in the docs rather than source, that will always show full names and all arguments, it also shows you the version generated by to_additive etc.