Zulip Chat Archive

Stream: new members

Topic: Determining namespace

Matej Penciak (Mar 06 2022 at 01:40):

This may be a really silly question, but I've found myself running into this a bunch while trying to learn/navigate through mathlib:

If I'm scrolling through a mathlib file in VS Code, is there an easy way to figure out what the namespace a particular definition is made in (or maybe even at an arbitrary cursor position) without having to scrolling up to the last place the author wrote namespace blah?

Yakov Pechersky (Mar 06 2022 at 01:48):


Damiano Testa (Mar 06 2022 at 07:22):

Continuing this, I would have also answered to use where. However, if I modify a file early on in the import hierarchy, even if simply to put in a #where and the undo the effect, this usually triggers recompilation of lean files.

Is there a way of accessing the namespace without modifying the file, even temporarily?

Eric Wieser (Mar 06 2022 at 13:05):

I think this is possible in Lean 4, but not lean 3

Eric Wieser (Mar 06 2022 at 13:05):

Ideally it would be shown as a breadcrumb in vscode, which IIRC is what the lean4 extension does.

Damiano Testa (Mar 06 2022 at 14:23):

Ok, thanks Eric for the answer!

I googled what breadcrumbs are, I think I understand and it looks like it would be just what would be useful here. I'll wait for Lean 4!

Henrik Böving (Mar 06 2022 at 14:38):

Eric Wieser said:

I think this is possible in Lean 4, but not lean 3

Yeah in Lean4 if you hover a declaration:

it shows the full namespace + type, although it wasn't always this way either.

Alex J. Best (Mar 06 2022 at 14:43):

In vscode it even shows the breadcrumb of the current namespace and even lemma in the header below the filename. I don't see that in your screenshot @Henrik Böving, do you know if there is a way to add that for your editor?

Henrik Böving (Mar 06 2022 at 14:44):

Ehhh I think I even purposely disabled breadcrumbs for lsp-mode in general because they annoy me but I have definitely seen them in other languages inside emacs with lsp-mode in the past.

Henrik Böving (Mar 06 2022 at 14:46):

image.png yup, just works :tm: (if its enabled :p)

Last updated: Dec 20 2023 at 11:08 UTC