We can add support for these features in TLA+ code:
- Go To Definition for constants
- Errors / warnings (from SANY)
within VS Code, Eclipse Che, Eclipse, Emacs, GNOME builder, and Atom. And any more IDEs that adopt the language server protocol in the future.
Resources