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

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

For this exact example, what’s wrong with:

RemoveElems(COND(_), q) == SelectSeq(q, LAMBDA x : ~COND(x))

SelectSeq is built in to Sequences.

Steve Glaser

On Dec 6, 2015, at 1:15 PM, Y2i <yur...@xxxxxxxxx> wrote:

I'm just curious if it is OK to rely on this feature or not?

It's getting really handy, like in the operator below that removes sequence elements that satisfy some condition:

RECURSIVE RemoveElems(_,_)

RemoveElems(COND(_), q) ==

    IF q = <<>> THEN <<>>

    ELSE LET h == Head(q)

         IN  IF COND(h) 

                 THEN RemoveElems(COND, Tail(q)) 

                 ELSE <<h>> \o RemoveElems(COND, Tail(q))

LLL == RemoveElems(LAMBDA x : x = 4, <<5,3,6,7,4,3,4,5,7,8,2,1>>)

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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.