Zulip Chat Archive

Stream: lean4

Topic: Go to definition by clicking on link vscode

Shreyas Srinivas (Nov 22 2023 at 23:42):

When I hover over a definition, I get a documentation snippet along with where the definition is located. Is there a vscode way to open the definition inside vscode?

Alex J. Best (Nov 22 2023 at 23:58):

Are you looking for ctrl+click?

Alex J. Best (Nov 22 2023 at 23:58):

Or right click and go to definition?

Shreyas Srinivas (Nov 23 2023 at 00:00):

No I know these. But in other languages when I get the equivalent of the box showing me the docstring and module name, I also get a peek definition link in that same box

Patrick Massot (Nov 23 2023 at 00:16):

Ctrl-shift-F10?

Shreyas Srinivas (Nov 23 2023 at 00:18):

Patrick Massot said:

Ctrl-shift-F10?

That combination didn't do anything.

Patrick Massot (Nov 23 2023 at 00:25):

Maybe I misunderstood your question. Here an example of hitting Ctrl-shift-F10
peek.gif

Shreyas Srinivas (Nov 23 2023 at 00:29):

Patrick Massot said:

Maybe I misunderstood your question. Here an example of hitting Ctrl-shift-F10
peek.gif

I don't get this view you are getting.

Shreyas Srinivas (Nov 23 2023 at 00:31):

Oh right. For some reason it is Alt + F12 on my machine.

Shreyas Srinivas (Nov 23 2023 at 00:34):

This fixes my issue. Thanks. I am using the peek submenu: image.png

Last updated: Dec 20 2023 at 11:08 UTC