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

Re: [tlaplus] Generating sequences of functions

On 10/4/21 4:04 PM, Markus Kuppe wrote:

{ <<e>> : e \in [user: 1..3, amount: 1..6]} \cup {<<>>}

Apologies, I didn't read your example carefully.

Use Isaac's solution or

  SeqOf([user: 1..3, amount: 0..6], 3)

with  SeqOf  from the CommunityModules [1].


[1] https://github.com/tlaplus/CommunityModules/blob/913ba86e3e5a40d5b37b8adb1b1f4883cbe62ef4/modules/SequencesExt.tla#L34-L39

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/48b0f899-42e0-ce2a-1cc9-2e1aa624c6a3%40lemmster.de.