Markus Alexander Kuppe

@hwayne You requested this feature—could you take a look and help with the review?

> I would like to abandon this PR and replace it with a new clean one (& use the tree-sitter). It will be cleaner and more reliable, I think. >...

> I would argue the inconsistencies between regexes and SANY are far, far larger than any inconsistency between tree-sitter and SANY, since both conform almost entirely to the syntactic test...

Architecturally, will tree-sitter work in the VSCode browser mode on e.g. github.dev?

> tree-sitter-tlaplus can be compiled to webassembly (which is what Spectacle uses) but that has a different API than the NPM package I think. @ahelwer Are there any disadvantages to...

> @ahelwer Are there any disadvantages to using the WebAssembly API? @ahelwer Are there any disadvantages to using WebAssembly locally?

It seems to me that **tree-sitter-tlaplus** brings quite a bit of overhead. I don’t think we want to end up with an extension that’s either platform-specific or significantly larger than...

@muenchnerkindl What's your feeling? Can TLAPS (with the enablement branch) prove the liveness property Convergence given the specified fairness constraint? https://github.com/tlaplus/Examples/blob/3debf309d1d1afe33baca0f20f93821737b0307c/specifications/FiniteMonotonic/CRDT.tla

@muenchnerkindl What's your feeling? Can TLAPS (with the enablement branch) prove the liveness property `Convergence` given the specified fairness constraint? https://github.com/tlaplus/Examples/blob/3debf309d1d1afe33baca0f20f93821737b0307c/specifications/FiniteMonotonic/CRDT.tla

@muenchnerkindl wrote the following TLAPS proof: ```tla ------------------------------- MODULE CRDT --------------------------------- EXTENDS Naturals, FiniteSets, NaturalsInduction, TLAPS CONSTANT Node ASSUME NodeAssumption == IsFiniteSet(Node) VARIABLE counter vars == counter TypeOK == counter...