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

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

From: Leslie Lamport <tlapl...@xxxxxxxxx>
Date: Thu, 22 Nov 2018 12:37:56 -0800 (PST)
References: <F5511BD6-5315-4626-B230-7F00BC5CEB07@mailworks.org> <17E12ABA-DB0F-4ECF-8499-2941E69A72BE@gmail.com> <1c686cad-33c9-4ce8-9bca-5ffe265ab064@googlegroups.com>

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.)

Leslie

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

...

Is this distinction documented anywhere?

References:
- \in works, while \subseteq gives a “identifier undefined” error
  - From: Philip White
- Re: [tlaplus] \in works, while \subseteq gives a “identifier undefined” error
  - From: Stephan Merz
- Re: [tlaplus] \in works, while \subseteq gives a “identifier undefined” error
  - From: Philip White

Prev by Date: Re: [tlaplus] \in works, while \subseteq gives a “identifier undefined” error
Next by Date: "A label may not appear in a macro"
Previous by thread: Re: [tlaplus] \in works, while \subseteq gives a “identifier undefined” error
Next by thread: "A label may not appear in a macro"
Index(es):
- Date
- Thread