[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] \in works, while \subseteq gives a “identifier undefined” error
Stephan, thank you for the reply.
It sounds like you're saying that TLA+/TLC interprets "\in" as an assignment, while it interprets "\subseteq" as a regular state predicate (non-assignment).
So to make my initial condition work, I need to find an expression in the form of "=" or "\in", hence what you suggested with "\in SUBSET".
Do I have it right?
Is this distinction documented anywhere?