fixing library_note references

Stream: mathlib4

[Thomas Murrills]

Do library notes currently work? If so, how should references to them (e.g. note [reducible non-instances] be formatted in mathlib4?

[Mario Carneiro]

just like that

[Thomas Murrills]

Ok, neat. I noticed I couldn't command-click them like I can in mathlib, so I thought they might be formatted incorrectly.

[Mario Carneiro]

Not sure what we have to do to make that work (cc: @Gabriel Ebner ?)

[Gabriel Ebner]

Go-to-definition was implemented in the vscode extension without any help from the server. Maybe we can do something fancier directly in the server in the future, but for now we could also just copy the code from the Lean 3 vscode extension.