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

Re: Tagged formulas

I don't use Capture(x, Action)', but rather Action(t) is my subaction, _within which_ I can now use the parameter t in any formula -- primed or not -- and know that it's a constant that is equal to the current value of x. 

So, if

    VARIABLE x, y
    Foo(a) == a + y

I can do:

    Next == Capture(x, LAMBDA t:
        /\ ... Foo(t) ....  \* = x + y
        /\ ...
        /\ ... Foo(t)' ....) \* = x + y'

So Capture is a capturing/lowering LET (with the caveat that it can only be used in binary valued formulas), which is exactly what I wanted.