[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Can the VSCode TLA+ extension do Unicode autocomplete?

From: 'Miguel Raz-Guzmán Macedo' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Date: Sat, 29 Nov 2025 16:49:59 -0800 (PST)

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/0790b81b-8600-4ec4-9695-9a60e1006170n%40googlegroups.com.

Follow-Ups:
- Re: [tlaplus] Can the VSCode TLA+ extension do Unicode autocomplete?
  - From: Andrew Helwer

Prev by Date: [tlaplus] Re: TLA+ repo on Google CodeWiki?
Next by Date: Re: [tlaplus] Can the VSCode TLA+ extension do Unicode autocomplete?
Previous by thread: Re: [tlaplus] Prove properties of the form [](P => []P) with TLAPS
Next by thread: Re: [tlaplus] Can the VSCode TLA+ extension do Unicode autocomplete?
Index(es):
- Date
- Thread