Hello Andrew,
The book "Specifying Systems"[1] has a description and the semantics of the
built-in operators of TLA+ in chapter 16 (p.291). The error message might be a
bit confusing because built-in operators do not need to live in their own
module, that's just how TLC handles it.
cheers,
Martin
[1] https://lamport.azurewebsites.net/tla/book.html
On 4/21/21 5:56 PM, Andrew Helwer 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
> <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tlaplus/e66c183c-d270-4807-9d2a-fab593539cbbn%40googlegroups.com
> <https://groups.google.com/d/msgid/tlaplus/e66c183c-d270-4807-9d2a-fab593539cbbn%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/83f97890-d829-2d7b-c16a-c0568cd86d75%40gmail.com.