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

[Emanuel Koczwara <emanuel.koczwara@xxxxxxxxx>]

Hi,

  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.

  Right?

  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?

Thanks,

Emanuel

-- 
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.