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

*From*: Emanuel Koczwara <emanuel.koczwara@xxxxxxxxx>*Date*: Sun, 26 Jul 2020 05:18:41 -0700 (PDT)*References*: <0dd33769-a76b-4ffc-a201-ffaacad1e50eo@googlegroups.com> <2b1a67eb-1e58-4b8d-9858-5a5aa61fce9dn@googlegroups.com>

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.

**Follow-Ups**:**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?***From:*ron.pr...@xxxxxxxxx

**References**:**[tlaplus] The rules of TLA+ do not imply that 1 /= "a" ?***From:*Emanuel Koczwara

**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?***From:*ron.pr...@xxxxxxxxx

- Prev by Date:
**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?** - Next by Date:
**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?** - Previous by thread:
**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?** - Next by thread:
**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?** - Index(es):