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

[tlaplus] util module


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!


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e70726dc-a969-40cb-9779-6bd8948590e7%40googlegroups.com.