Re: Recursive definitions of higher-order operators

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

It seems to work, but only if the operator argument is in the first position:

    RECURSIVE FlatMap(_, _)

    FlatMap(F(_), seq) == IF Len(seq) = 0 THEN <<>> ELSE F(Head(seq)) \o FlatMap(F, Tail(seq)) 

TLC handles it too.