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

Re: Tagged formulas

Yes, of course; I meant primed.

After some experimentation, I now  understand my problem better. Suppose I have these declarations:

    VARIABLES x, y
    Foo(a) == a \cup y

If I then use the primed formula Foo(x)', it will prime both x and y, but in my situation only y' is already determined in the evaluation, so TLC will emit the usual error in such cases, "The identifier x is either undefined or not an operator".

Trying to get around this seems to be of no use:

    LET t == x IN Foo(t)'

yields the same result. Other transformations don't change the situation:

    LET t == x[5].a \cap {2, 3} IN Foo(t)'

Is there a way to capture a value from a variable and pass it into a formula in such a way that priming it will not try to lazily obtain the value from the variable (or, simply put, "forget" the value's dependence on the variable)? While I see the merits of such evaluation, it can also be quite confusing (as in my case), because the value passed to the function is a result of several non-trivial transformations, that it's easy to miss the value's dependence on a variable.