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.
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.
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.
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:
*.conf files should not be under version control.
Thanks! I used version 1.11, I've not upgraded to 1.12 yet.
Last updated: Feb 08 2023 at 04:04 UTC