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

Re: Tagged formulas

Hi Ron,

I should point out another problematic part of what you wrote--namely:

   <<s, t>>[[(CAPTURE e)']] = 1

The semantics of prime is that

   <<s, t>>[[exp']] = t[[exp]].

Therefore, your equality implies that t[[CAPTURE e]] = 1.  Why does
t[[x]] = 2 imply that t[[CAPTURE x]] = 1?