vscode-tlaplus icon indicating copy to clipboard operation
vscode-tlaplus copied to clipboard

"Go to definition" for definitions in module extended

Open lemmy opened this issue 4 years ago • 1 comments

Let B be a module and E be an extender (EXTENDS B). Clicking Go to definition on a symbol in E that is defined in B doesn't work.

Peek 2020-12-10 10-57

lemmy avatar Dec 10 '20 18:12 lemmy

Related: https://github.com/alygin/vscode-tlaplus/issues/218

lemmy avatar Nov 03 '21 20:11 lemmy