Re: [tlaplus] Recursive definitions of higher-order operators

[Y2i <yur...@xxxxxxxxx>]

By using the trick in SelectSeq and Cardinality, I got a version of FlatMap that uses recursive functions instead of recursive operators:

FlatMap(seq, F(_)) ==

    LET G[i \in 0..Len(seq)] == IF i = 0 THEN <<>> ELSE G[i-1] \o F(seq[i])

    IN G[Len(seq)]

This is the version I'll be using for my work.

Yuri