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

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

Chapter 14 of Specifying Systems explains how TLC works and what kind of specifications it can handle.  (It does not document the approximately infinite number of ways of writing specifications that TLC can't handle.)


On Thursday, November 22, 2018 at 12:32:36 PM UTC-8, Philip White wrote:

Is this distinction documented anywhere?