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!AndrewOn Sat, Nov 29, 2025 at 4:50 PM 'Miguel Raz-Guzmán Macedo' via tlaplus <tla...@xxxxxxxxxxxxxxxx> 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...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/0790b81b-8600-4ec4-9695-9a60e1006170n%40googlegroups.com.