VSCode plug-in type class navigation

Stream: new members

[Rado Kirov]

In the few examples I tried in VS Code when one clicks on a type class variable it leads to the class definition. In cases where the instance should be known due to arguments, why doesn't cmd+click navigate straight to the instance?

I looked around and found #synth that basically does what I want, but it requires me to exact to a new line.

[Marc Huisinga]

Fixing this is on my to-do list with p-high. I might get to it next quarter.

[Rado Kirov]

Awesome. If it's mostly a pure TS task for https://github.com/leanprover/vscode-lean4 I might be able to help (if you give me a bit of a blueprint in an github issue). Curiously enough, it seems the haskell extension also doesn't navigate to instances, but type classes might be more dynamic in haskell?

[Marc Huisinga]

It is not a pure TypeScript task and requires some fairly non-trivial language server changes.