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

Re: [tlaplus] util module



On 15.11.19 15:14, isaacdefrain@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].

M.

[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/a84f6f80-d46b-ad82-1062-cc25583d360c%40lemmster.de.