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

Re: [tlaplus] Flattening a tuple of tuples

On 6/30/21 8:55 AM, Hillel Wayne wrote:
From the community modules we have FoldLeft <https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla>. Then we can write flatten as

Flatten(seq) == FoldLeft(LAMBDA x, y: x \o y, <<>>, seq)

As an old school, more readable recursive function:

EXTENDS Naturals, Sequences

Flatten(seq) ==
   LET F[ i \in 0..Len(seq)] == \* 0 to handle seq=<<>>
      IF i = 0
      THEN <<>>
      ELSE F[i-1] \o seq[i]
   IN F[Len(seq)]

It's likely faster for TLC to evaluate until at least Folds!MapThenFoldSet gets a module override.


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/53c3adad-d1cf-8bae-8143-bd2840af0b78%40lemmster.de.