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

Re: Tagged formulas

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.


On Wednesday, January 6, 2016 at 9:39:20 AM UTC-8, Ron Pressler wrote:
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?