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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Thu, 7 Jan 2016 03:37:50 -0800 (PST)*References*: <71319d03-6ab4-48a7-a6a2-53e7c9c48a51@googlegroups.com> <77ff66be-f3e5-4c2f-8906-28ebb049baae@googlegroups.com>

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.

Ron

**Follow-Ups**:**Re: Tagged formulas***From:*Ron Pressler

**References**:**Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Leslie Lamport

- Prev by Date:
**Re: dot/graphviz visualization for TLC** - Next by Date:
**Re: Recursive definitions of higher-order operators** - Previous by thread:
**Re: Tagged formulas** - Next by thread:
**Re: Tagged formulas** - Index(es):