[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: What operators are defined in TLA+ BUILTINS?
Oh yes I meant the BNF grammar specifically, not the entirety of the language spec. Makes sense they are captured by the identifier token instead of having their own rule.
I looked through the codebase and can't find where these builtins get special treatment, but wherever I find BOOLEAN I also find TRUE, FALSE, and STRING, so Leslie you're probably right that is all of them.
Andrew
On Wednesday, April 21, 2021 at 12:22:27 PM UTC-4 Leslie Lamport wrote:
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
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?
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/dff8101d-a028-4fc3-8000-f4a1dc829b1dn%40googlegroups.com.