It is questionable how much of a bug this is because both of these failures should be rejected at the semantic level since \X and \times are built-ins; however, a straightforward reading of the TLA+ syntax grammar shows these should be accepted at the syntax level at least. Both of these test inputs will fail:
---- MODULE Test ----
x \X y == 0
x \times y == 0
====
This bug can fall under the category of "low priority" or possibly even be kicked up to the language standard level to decide to what extent Cartesian products should be treated as regular infix operators for syntax parsing purposes.
It is questionable how much of a bug this is because both of these failures should be rejected at the semantic level since
\Xand\timesare built-ins; however, a straightforward reading of the TLA+ syntax grammar shows these should be accepted at the syntax level at least. Both of these test inputs will fail:This bug can fall under the category of "low priority" or possibly even be kicked up to the language standard level to decide to what extent Cartesian products should be treated as regular infix operators for syntax parsing purposes.
Ref #159