Re: [tlaplus] Flattening a tuple of tuples

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.

M.

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