Zulip Chat Archive

Stream: new members

Topic: Getting the current namespace in vscode


view this post on Zulip 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?

view this post on Zulip Rob Lewis (Jul 29 2020 at 17:27):

#where

view this post on Zulip Eric Wieser (Jul 29 2020 at 18:09):

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

view this post on Zulip 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

view this post on Zulip 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: May 14 2021 at 23:14 UTC