In vscode, when I control-click on an identifier in infoview, it jumps to definition.
It would be nice if this worked in lean4web also. I assume a similar interception would have to be added to the way that identifiers in the editor pane jump to mathlib docs.
In vscode, when I control-click on an identifier in infoview, it jumps to definition.
It would be nice if this worked in lean4web also. I assume a similar interception would have to be added to the way that identifiers in the editor pane jump to mathlib docs.