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

[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?


  This rises some more questions:

  * How is equality/unequality defined actually?

    ** What about '1 = 2' and 1 /= 2?
    ** What about '1.0 = 1' and 1.0 /= 1?
    ** What about '3.14 = 1' and 3.14 /= 1?

  As far as I know, every value is a set in TLA+.
  We just don't care what the elmenets are in 1, 3.14 etc.


  As far as I know, sets are equal if they have the same elements.
  This means, that we can't compare sets of unknown elements.

  * So what we can compare?
  * Why Len() from Sequences works as expected?


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/a95b6583-6bc5-44a5-9521-af3daa7c62fbo%40googlegroups.com.