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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Thu, 11 Jan 2024 07:53:02 -0800*References*: <d4b8a84a-4296-4583-85a5-76cfec10ffacn@googlegroups.com> <b8a1f8e5-f668-45c5-a717-4f9f4ed42e3en@googlegroups.com> <fe903045-ea10-4983-a10f-4e315df185e7n@googlegroups.com> <30D2B8D1-41AF-4FCF-86C3-4B95D9207F98@lemmster.de> <d7b9cde8-9573-4fe8-9bda-36bd9ca32289n@googlegroups.com>

https://www.youtube.com/watch?v=w9t6JnmxV2E (more details at https://github.com/tlaplus/CommunityModules/?tab=readme-ov-file#how-to-use-it) Markus > On Jan 11, 2024, at 2:20 AM, christin...@xxxxxxxxx <christina.a.burge@xxxxxxxxx> wrote: > > Thanks! That fixed it :) I have one further (and very silly) question - how do I actually use the functions defined in the community modules, the toolbox doesn't recognise, for example Divides, from the DyadicRadtionals module. I have added an EXTENDS DyadicRationals to my spec, but this hasn't helped. Is it because Divides is "LOCAL"? But then how could you use it at all? I can't seem to find the answer anywhere else! -- 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/D4CEAE38-5CF2-4CAA-B13F-1B0BC205221C%40lemmster.de.

**References**:**[tlaplus] Checking matrix multiplication correctness***From:*christin...@xxxxxxxxx

**[tlaplus] Re: Checking matrix multiplication correctness***From:*Andrew Helwer

**[tlaplus] Re: Checking matrix multiplication correctness***From:*christin...@xxxxxxxxx

**Re: [tlaplus] Checking matrix multiplication correctness***From:*Markus Kuppe

**Re: [tlaplus] Checking matrix multiplication correctness***From:*christin...@xxxxxxxxx

- Prev by Date:
**Re: [tlaplus] Checking matrix multiplication correctness** - Next by Date:
**[tlaplus] Re: Draft of New TLA Book** - Previous by thread:
**Re: [tlaplus] Checking matrix multiplication correctness** - Next by thread:
**[tlaplus] Where to put proofs on a SetSum?** - Index(es):