Stream: new members
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):
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: May 14 2021 at 23:14 UTC