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

Re: [tlaplus] util module

Thank you for your quick response and helpful suggestion, Markus!

On Friday, November 15, 2019 at 8:10:42 PM UTC-5, Markus Alexander Kuppe wrote:
On 15.11.19 15:14, isaacd...@xxxxxxxxx wrote:
> 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 should ask the author of the spec to send you the util module. A
"util" module is not part of the standard modules or the community
modules [1].


[1] https://github.com/tlaplus/CommunityModules

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/592ba8b3-c3e4-4df9-9d1f-40e453ff7a02%40googlegroups.com.