On 02/15/11 12:38, Paul Eggert wrote:
>>>  invariant (X)?

gl_assume(X) seems like a good choice to me.
"invariant" doesn't imply that "X" is either true or false
and, as Paul said, the expression need not be constructed of
invariant components.  Yes, the result should be invariant
(invariant-true or invariant-false?), but it is fuzzy.
"gl_assume()" seems pretty clear to me.....

Reply via email to