Zulip Chat Archive

Stream: new members

Topic: Getting the current namespace in vscode


Eric Wieser (Jul 29 2020 at 17:26):

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 (Jul 29 2020 at 17:27):

#where

Eric Wieser (Jul 29 2020 at 18:09):

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

Alex J. Best (Jul 29 2020 at 18:11):

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

Alex J. Best (Jul 29 2020 at 18:13):

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.


Last updated: Dec 20 2023 at 11:08 UTC