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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 6 Apr 2021 12:19:31 +0200*References*: <52111fcc-e8df-469e-8894-c113ae398056n@googlegroups.com>

Hello, I am not trying to understand your definition but simply suggest how to make it syntactically legal. In the syntactic form { e : x \in S, y \in T } the identifier x is not allowed to occur in S or T (cf. Specifying Systems, section 16.1.6). You must therefore use a nested set comprehension as in ... ELSE LET Extend(m) == { <<m>> \o l : l \in LinearExtensionsUtil(...) } IN UNION { Extend(m) : m \in Minimal(...) } (Of course, you do not actually need to use a LET but can also replace the use of Extend in the body by its definition. However, I find it easier to read in this way.) 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/555B8BE7-2060-4E6F-B2DE-F609ABD05E62%40gmail.com. |

**Follow-Ups**:

**References**:

- Prev by Date:
**[tlaplus] How to generate all possible linear extensions (i.e., topological sortings) of a partial order?** - Next by Date:
**Re: [tlaplus] How to generate all possible linear extensions (i.e., topological sortings) of a partial order?** - Previous by thread:
**[tlaplus] How to generate all possible linear extensions (i.e., topological sortings) of a partial order?** - Next by thread:
**Re: [tlaplus] How to generate all possible linear extensions (i.e., topological sortings) of a partial order?** - Index(es):