[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: What operators are defined in TLA+ BUILTINS?
- From: Leslie Lamport <tlaplus.ll@xxxxxxxxx>
- Date: Wed, 21 Apr 2021 09:22:27 -0700 (PDT)
- Ironport-hdrordr: A9a23:8yFGJ6k56kqAlvCke1aZ4ai8xbLpDfIK3DAbvn1ZSRFFG/GwvcaogfgdyFvImC8cMUtPpfmsMLSNKEmyybdb+o8UVI3OYCDDtHGzJI9vqavOqgeKJwTb9upQkZhtaLJ/DtqYNzhHpP336gW5DNosqePvmJyAv/vUzHtmUGhRAZ1I0gERMGqmO3wzYAFHAJYjfaD82vZ6
- References: <email@example.com>
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.
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?
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/c16d3ed7-02ff-45e9-b871-67b8e3822772n%40googlegroups.com.