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

[Stephan Merz <stepha...@xxxxxxxxx>]

Ah, but you can define it using a recursive function:

Range(s) == {s[i] : i \in DOMAIN s}

FlatMap(F(_), seq) ==

  LET FM[s \in Seq(Range(seq))] == 

        IF s = << >> THEN << >> ELSE F(Head(s)) \o FM[Tail(s)] 

  IN  FM[seq]

SelSeq(seq, Test(_)) == FlatMap(LAMBDA e : IF Test(e) THEN <<e>> ELSE <<>>, seq)

I just had TLC evaluate that SelSeq(<<0,1,2,3,4,5>>, LAMBDA i : i % 2 = 0) = <<0,2,4>>

Stephan