Hello,
Thank you for taking time to help!
Let me preface my question with: I have just started learning TLA+. I downloaded the zip 1.6.0 version and started two days ago.
I'm looking at a spec that starts with the statement: EXTENDS Integers, Sequences, util
My first question is what is this util module? Where is it located? TLA+ returns a parsing error due to it...
To naively troubleshoot, I commented it out and apparently it contains Options and the functions SeqToSet, SetToSeq, and MapSeq. I haven't been able to find any information about these functions, though the first two may be more or less obvious, from what I can tell it seems like MapSeq: Record x Seq -> Seq. What I am I missing here?
Any help/suggestions would be greatly appreciated! Thank you!
Best,
Isaac