Re: [tlaplus] \in works, while \subseteq gives a “identifier undefined” error

[Philip White <phi...@xxxxxxxxxxxxx>]

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?

Thanks.