Bring back `library_note`s?
Opened this issue · 0 comments
mo271 commented
Are there plans to support library_note in the same way it was for lean3 (ctrl-click on the note to jump to it).
See
https://github.com/leanprover/vscode-lean4/blob/e0870d3eba00985f17563bdc1ce990964cb0952e/vscode-lean4/old/src/librarynote.ts