[tlaplus] Re: Unicode TLA+

[Alexander Niederbühl <a.niederbuehl@xxxxxxxxx>]

I think this would be very useful, I find the ASCII representation a bit verbose and distracting. I know of several people who feel the same, e.g. https://matklad.github.io/2020/11/01/notes-on-paxos.html as another data point. Currently I'm using a VSCode extension together with FiraCode as workaround.

A bit unrelated but since in TLA+ there are many ways to write the same thing like \cup, \union or /= , # and different ways to format the code in terms of line breaks etc. I wish there would be a tool to get a canonically formatted Unicode representation which ideally TLC would be able to check. Do you think the treesitter grammar could be utilized to build a code formatter similar to prettier in _javascript_ or black in Python?

 

-- 
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 on the web visit https://groups.google.com/d/msgid/tlaplus/9b03ad90-b045-4678-95df-2a392f0b807bn%40googlegroups.com.