Can the VSCode TLA+ extension do Unicode autocomplete?

[Miguel Raz-Guzmán Macedo]

If I'm writing in Lean4, the Lean4 extension will detect when I type `\in` and replace it (with an optional TAB press) into ∈.

Am I being very silly or is there no way to turn on this behaviour in the VSCode extension?

[Andrew Helwer]

Correct, the VS Code extension does not have such a feature. It currently only exists for Neovim (https://github.com/tlaplus-community/tlaplus-nvim-plugin) and emacs (https://github.com/bugarela/tla-input). If you would be interested in implementing it for the VS Code extension, that would be a wonderful gift to the community!

Andrew

On Sat, Nov 29, 2025 at 4:50 PM 'Miguel Raz-Guzmán Macedo' via tlaplus <tla...@googlegroups.com> wrote:

If I'm writing in Lean4, the Lean4 extension will detect when I type `\in` and replace it (with an optional TAB press) into ∈.

Am I being very silly or is there no way to turn on this behaviour in the VSCode extension?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/0790b81b-8600-4ec4-9695-9a60e1006170n%40googlegroups.com.

[Miguel Raz-Guzmán Macedo]

Deal :)

First typescript PR ever, so if anyone can help get it over the finish line I'd appreciate it.

https://github.com/tlaplus/vscode-tlaplus/pull/468