[tlaplus] Is it possible to generate tuple sequence?

[Dmytro Ivanov <dmytro@xxxxxxxxxxxxxx>]

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

Thanks!

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