Re: [tlaplus] Checking matrix multiplication correctness

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.