vscode-lean4 icon indicating copy to clipboard operation
vscode-lean4 copied to clipboard
verified publisher icon leanprover

Bring back `library_note`s?

Open mo271 opened this issue 2 years ago • 0 comments

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

mo271 avatar Feb 18 '23 22:02 mo271