Daniel Kirk (Jan 05 2021 at 14:43): Daniel Kirk (Jan 05 2021 at 14:43):Hi all, hope everyone had a relaxing Christmas and new year's break.
I'm releasing a functional iteration of my implementation of free-left-modules, bases (both finite and infinite) and (finite) direct sums of modules extending Mathcomp's lmodType.
https://github.com/Modularius/MathcompFreeModules
It currently compiles and works however I'm hoping someone with more knowledge can help explain why I'm getting warnings for several of the canonical declarations claiming they are redundant. I'm not at all sure why this happens or what it means, I'm still learning the particulars of canonical structures.
Daniel Kirk (Jan 05 2021 at 14:44):There are commented notes in the .v files that should give a good overview of what the files do. I'd be very grateful to anyone who tries them out.
Karl Palmskog (Jan 05 2021 at 14:54):you probably want to specify which MathComp version you're compatible with and add some continuous integration to check that. See here for boilerplate/examples:
In particular, *.conf files should not be under version control.
Daniel Kirk (Jan 05 2021 at 19:15):Thanks! I used version 1.11, I've not upgraded to 1.12 yet.
Last updated: Sep 25 2023 at 12:01 UTC