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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Thu, 7 Jan 2016 14:42:51 -0800 (PST)*References*: <71319d03-6ab4-48a7-a6a2-53e7c9c48a51@googlegroups.com> <20d67976-47a3-440d-942e-51f3b035554e@googlegroups.com> <393668fc-f7ac-49ad-9f04-598c39d1a771@googlegroups.com>

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!

**Follow-Ups**:**Re: Tagged formulas***From:*Leslie Lamport

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

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

**Re: Tagged formulas***From:*Ron Pressler

- Prev by Date:
**Re: Tagged formulas** - Next by Date:
**Re: Tagged formulas** - Previous by thread:
**Re: Tagged formulas** - Next by thread:
**Re: Tagged formulas** - Index(es):