tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
67 stars 20 forks source link

TLAPM does not parse quantifiers using `\forall` or `\exists` keywords instead of `\A` or `\E` #160

Open ahelwer opened 3 weeks ago

ahelwer commented 3 weeks ago

Thanks to @muenchnerkindl for remembering this; opening an issue for tracking. This will fail at the syntax parse level:

---- MODULE Test ----
op == \forall x, y \in Nat, z \in Int, a, b, c \in Real : FALSE
op == \exists x, y \in Nat, a, b \in Int : TRUE
====

While this will succeed:

---- MODULE Test ----
op == \A x, y \in Nat, z \in Int, a, b, c \in Real : FALSE
op == \E x, y \in Nat, a, b \in Int : TRUE
====

Ref #159