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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 16 Aug 2022 12:03:11 +0200*References*: <09b86764-7c37-4c9b-b120-982a0018d9dcn@googlegroups.com> <9B4878A6-3141-4D83-AA54-DF2762A26412@gmail.com> <c3ddcc2c-c36d-45a8-b9c3-3f936364f963n@googlegroups.com>

In formulas Q x \in S : F (where Q is either \A or \E), S has to be a set. See also section 1.3 of "Specifying Systems". TLA+ is not like Python where conversions are implicit. Stephan
--
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/52E5A0D9-D456-4A51-9959-90E9C837FC29%40gmail.com. |

**References**:**[tlaplus] IS there any way of applying \A and \E on sequences in PlusCa l? <EOM>***From:*Anand Kumar

**Re: [tlaplus] IS there any way of applying \A and \E on sequences in PlusCa l? <EOM>***From:*Stephan Merz

**Re: [tlaplus] IS there any way of applying \A and \E on sequences in PlusCa l? <EOM>***From:*Anand Kumar

- Prev by Date:
**Re: [tlaplus] IS there any way of applying \A and \E on sequences in PlusCa l? <EOM>** - Next by Date:
**[tlaplus] Raft: followers don't reply always upon an AppendEntriesRequest** - Previous by thread:
**Re: [tlaplus] IS there any way of applying \A and \E on sequences in PlusCa l? <EOM>** - Next by thread:
**[tlaplus] Raft: followers don't reply always upon an AppendEntriesRequest** - Index(es):