[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,
Yuri