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

["'Martin' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

Hello Paolo,

The list you referenced contains all operator names that have some special
treatment (e.g. also all infix operators are included in the table or lexemes
neccessary for writing proofs). If you just need a new operator name that table
is perfect for checking collisions. But it's not a problem to write

EXTENDS Naturals

a \sim b == (a-b) % 2 == 0  \* a ~ b are congruent modulo two

even though \sim is listed.

cheers,
Martin


On 4/21/21 6:14 PM, Paulo Feodrippe wrote:
> 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
> <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
> <mailto: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
>     <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%2Bunsubscribe@xxxxxxxxxxxxxxxx>
>     > <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx
>     <mailto:tlaplus%2Bunsubscribe@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>
>     >
>     <https://groups.google.com/d/msgid/tlaplus/e66c183c-d270-4807-9d2a-fab593539cbbn%40googlegroups.com?utm_medium=email&utm_source=footer
>     <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
>     <mailto:tlaplus%2Bunsubscribe@xxxxxxxxxxxxxxxx>.
>     To view this discussion on the web visit
>     https://groups.google.com/d/msgid/tlaplus/83f97890-d829-2d7b-c16a-c0568cd86d75%40gmail.com
>     <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
> <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tlaplus/CANDKcwDHORK-jrnEMRoPoeon5Pn3Tg2LW64ovn3TQ-hmXGbUHA%40mail.gmail.com
> <https://groups.google.com/d/msgid/tlaplus/CANDKcwDHORK-jrnEMRoPoeon5Pn3Tg2LW64ovn3TQ-hmXGbUHA%40mail.gmail.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/56522b9a-8a90-66df-70ef-07b90bf10333%40gmail.com.