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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Wed, 6 Jan 2016 11:56:29 -0800 (PST)*References*: <71319d03-6ab4-48a7-a6a2-53e7c9c48a51@googlegroups.com>

I presume that by "tagged" you mean primed. Yes, e' means e with all variables in it primed. Please tell us exactly what TLC is not interpreting as you expect it to.

Leslie

On Wednesday, January 6, 2016 at 9:39:20 AM UTC-8, Ron Pressler wrote:

Hi.I seem to recall reading that in TLA+ a tagged formula means the formula with all variables tagged. TLC does not seem to be of the same opinion; as a result I sometimes find myself writing the same formula twice -- for the tagged and untagged variables. Did I misunderstand or is this a TLA+ feature unsupported by TLC?Ron

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

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

- Prev by Date:
**Re: dot/graphviz visualization for TLC** - Next by Date:
**Re: [tlaplus] Re: dot/graphviz visualization for TLC** - Previous by thread:
**Tagged formulas** - Next by thread:
**Re: Tagged formulas** - Index(es):