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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 19 Dec 2019 11:55:32 +0100*References*: <07e1f71b-14d3-4d36-abdc-e5c7be42cdc1@googlegroups.com>

Hello, first of all, note that {x : x \in 1..5} is just an obfuscated way of writing 1 .. 5. :-) There is not a unique sequence corresponding to a set, and that probably explains why TLA+ doesn't have syntax for sequence comprehension analogous to set comprehension. In particular, CHOOSE x \in Seq(1 .. 5) : TRUE (which TLC refuses to evaluate anyway) could denote any sequence containing the numbers 1 to 5, including << >>, <<1, 1, 4, 1>> etc. You can write a recursive operator that constructs a sequence containing exactly one copy of a finite set, as follows: RECURSIVE SeqFromSet(_) SeqFromSet(S) == IF S = {} THEN << >> ELSE LET x == CHOOSE x \in S : TRUE IN << x >> \o SeqFromSet(S \ {x}) It so happens that TLC evaluates SeqFromSet(1 .. 5) to the sequence <<1,2,3,4,5>>. Best, 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/2907DC3E-DB0C-434F-9293-334CDA201D31%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] Is it possible to generate tuple sequence?***From:*Dmytro Ivanov

- Prev by Date:
**[tlaplus] Is it possible to generate tuple sequence?** - Next by Date:
**Re: [tlaplus] Is it possible to generate tuple sequence?** - Previous by thread:
**[tlaplus] Is it possible to generate tuple sequence?** - Next by thread:
**Re: [tlaplus] Is it possible to generate tuple sequence?** - Index(es):