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

*From*: Isaac DeFrain <isaacdefrain@xxxxxxxxx>*Date*: Mon, 4 Oct 2021 17:16:02 -0600*Ironport-hdrordr*: A9a23:/h8vMKDLttE3EjrlHenL55DYdb4zR+YMi2TDsHoRdfU1SKKlfq+V7ZcmPHPP+VQssRIb9uxoRpPhfZq0z/cciuMs1NyZMDUO1lHEEL1f*References*: <CAN3aEu7h=uR+4EJSBNP9qMGWddzpkPFo8bccUjPeKFovob-tsQ@mail.gmail.com>

Hey Pablo,

If you only need an implicit (non-enumerable) definition, this will do the trick:

Seq_n(n, s) == { seq \in Seq(s) : Len(seq) <= n }

If you need an explicit definition, a recursive definition will do the trick:

RECURSIVE seq_n(_, _, _)

seq_n(n, s, acc) ==

IF n = 0 THEN acc

ELSE

LET next == { Append(a, x) : x \in s, a \in acc }

IN seq_n(n - 1, s, acc \cup next)

seq_n(n, s, acc) ==

IF n = 0 THEN acc

ELSE

LET next == { Append(a, x) : x \in s, a \in acc }

IN seq_n(n - 1, s, acc \cup next)

\* set of sequences of length at most n

Seq_n(n, s) == seq_n(n, s, {<<>>})

I hope this helps!

Best,

Isaac DeFrain

On Mon, Oct 4, 2021 at 4:35 PM pablo fernandez <fernandezpablo85@xxxxxxxxx> wrote:

--Hello!I have a function that represents a transaction:[user: 1..3, amount: 1..6]And would like to have the set of all sequences from 0 to 3 transactions, e.g:{<<>>, <<[user:1, amount: 0]>>, <<[user:1, amount: 0], [user:2, amount: 0]>> ... }How can I achieve this?Pablo

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/CAN3aEu7h%3DuR%2B4EJSBNP9qMGWddzpkPFo8bccUjPeKFovob-tsQ%40mail.gmail.com.

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/CAM3xQxHs7AsuL5towz30_6p8eT%3DypJGijnURv2EOg3MX8NBABA%40mail.gmail.com.

**References**:**[tlaplus] Generating sequences of functions***From:*pablo fernandez

- Prev by Date:
**Re: [tlaplus] Generating sequences of functions** - Next by Date:
**Re: [tlaplus] Generating sequences of functions** - Previous by thread:
**Re: [tlaplus] Generating sequences of functions** - Next by thread:
**[tlaplus] How is this successful?** - Index(es):