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

[tlaplus] Is it possible to generate tuple sequence?

Hi everyone :) Learning TLA+ and have a question about sequences:

If I have a set of valid values, for example foo == {x : x \in 1..5}
How can I generate some sequence of this values in PlusCal?

Currently I just hardcoded bar = << 1, 2, 3, 4, 5 >> and that works.
I've also tried bar = << x \in foo : TRUE >> but that's not supported. Tried bar = CHOOSE x \in Seq(foo) : TRUE but that doesn't for because Seq(foo) is not itereable ..


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/07e1f71b-14d3-4d36-abdc-e5c7be42cdc1%40googlegroups.com.