[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable
Dear Dominik and Stephan,
Thank you for your quick help. Dominik's BoundedSeq worked!
I was not sure that BoundedSequence would contain elements of Data because, for some reason, I thought it would be a set of functions [x->Data]. But TLC said that this invariant Len(q) > 0 => Head(q) \in Data was correct. I should probably hold off my questions until after I finish Chapter 14 :)
Thank you again,