Determining namespace

Stream: new members

[Matej Penciak]

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]

#where

[Damiano Testa]

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]

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

[Eric Wieser]

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

[Damiano Testa]

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]

Eric Wieser said:

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

Yeah in Lean4 if you hover a declaration:
image.png

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

[Alex J. Best]

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]

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]

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