[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] What operators are defined in TLA+ BUILTINS?



Besides the book and if you wanna check some TLC code, you can also see https://github.com/tlaplus/tlaplus/blob/d977051118f63b9c97d7d4c4d6af27183971ada3/tlatools/org.lamport.tlatools/src/tla2tex/BuiltInSymbols.java#L221

On Wed, Apr 21, 2021, 1:09 PM 'Martin' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:
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.

--
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/CANDKcwDHORK-jrnEMRoPoeon5Pn3Tg2LW64ovn3TQ-hmXGbUHA%40mail.gmail.com.