Zulip Chat Archive

Stream: lean4

Topic: Go to definition in infoview

Andrew Yang (Dec 04 2023 at 13:23):

Does "go to definition" work in infoview in lean4? It worked in lean3 but after upgrading to lean4 the rightclick menu looks like the following to me.
image.png

Johan Commelin (Dec 04 2023 at 13:25):

Ctrl-left-click should work

Andrew Yang (Dec 04 2023 at 13:29):

Thanks! Is this documented somewhere?

Alex J. Best (Dec 04 2023 at 13:39):

Not that I'm aware of, I also learned about it through zulip

Andrew Yang (Dec 04 2023 at 13:42):

Ah. And this also explains why vscode opens random pages when I want to copy from the infoview via ctrl-c.

Yaël Dillies (Dec 04 2023 at 13:42):

Yeah! That's super annoying behavior.

Eric Rodriguez (Dec 04 2023 at 13:44):

yeah, especially as there is no way to copy paste in the old ways

Scott Morrison (Dec 12 2023 at 00:38):

I've made an issue to record this https://github.com/leanprover/vscode-lean4/issues/374

Last updated: Dec 20 2023 at 11:08 UTC