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

Re: [tlaplus] Checking matrix multiplication correctness

https://www.youtube.com/watch?v=w9t6JnmxV2E (more details at https://github.com/tlaplus/CommunityModules/?tab=readme-ov-file#how-to-use-it)


> 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.