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

Re: Tagged formulas



BTW, your suggestion of `\E t : t = x` works quite well. At first I defined:

    Capture(var, Action(_)) == \E t \in S : t = var /\ Action(t) \* S is a constant set known to contain the variable var


and it does the capture/lowering I want.


Then I tried:


    Capture(var, Action(_)) == \E t \in {var} : t = var /\ Action(t)


and that works too! I guess that's because the quantification happens outside the priming, and so t is a fresh, bound symbol rather than an _expression_ involving a variable.


Thanks again!