There is no actual TLA+ Builtins module; that was apparently an easy way to report that TRUE is a TLA+ primitive. I'm not sure what you mean by "the language spec". TRUE does appear in Table 1 of "Specifying Systems". It's not part of the syntax specification because, syntactically, it's just an operator that takes no argument. The only other such built-in operators in that table are FALSE, BOOLEAN, and STRING. I can't think of any others, but perhaps someone can think of another one that isn't listed in that table that I have forgotten. I expect searching SANY's code for BOOLEAN would reveal it if it exists.
Leslie
On Wednesday, April 21, 2021 at 8:56:08 AM UTC-7 andrew...@xxxxxxxxx wrote:
The operator TRUE, for example, is not part of the language spec. However if you try to define it:
TRUE == 5
You get a parser error saying it is already defined in module --TLA+ BUILTINS--. What other operators are defined in this module?