Minutes 2025 05 28 - math-comp/math-comp GitHub Wiki
Questions for Georges
Yves does not think we have time to prepare questions Cyril and Pierre think it is not the right timing. Yves: Can we ask Georges to attend a future meeting? Cyril agrees.
Date for the 12th MC Sharing Day
Right now it conflicts with Rocq'n'share. Pierre proposes June 18th or July 2nd. Cyril not available July 2nd
PR triaging
- #1435 : Matteo explains his experiment on
monoid.v(see here) where he changes the subject of the structure from the operation to the type. He uses a new feature of HB, namely wrappers that are mixins that contain a factory on a (potentially) different subject. When defining a structure on some subject, we can use the factory on the other subject or the wrapper. Making an instance for one subject or the other declares both instances. - #1434 : adding modnMDXl, merged
- #1433 : #1256 duplicated some lemmas, this removes the duplicates. A few things get generalized, which makes some coercions non-uniform. Pierre: Let's not care. Cyril asks about the naming changes (
zmod_closedD->zmod_closed0Dandsubr_2closed->subr_closed). - #1420 : Cyril's first review was fixed, he is doing a second review.
Next Chair
Cyril