SSProve
Add documentation, clarification and optimization of the joy of state separating proofs
I mostly added comments, but also a new definition for a recurrent pattern and a Ltac tactic associated with it. The lagrange_poly_part_0 had an extra hypothesis that was not used in the proof, so I got rid of it. Same for some lemmas and definitions that were not used.
Thanks! As Lasse says a small table of contents, as is usual in MathComp might be helpful.
Here is a very detailed style guide for MC. No need to follow all of these now (especially the naming conventions), but it may give some guidance in the future... https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md
Should I add headers as the one in mathcomp, as the documentation suggest?
https://github.com/math-comp/math-comp/wiki/How-to-document
Yes, that would be great. Also, MC proofs are expected to be read while replaying them, so no need for elaborate documentation in proofs. However, helpful comments are always welcome.
On Thu, Apr 3, 2025 at 9:25 AM ErVinuelas @.***> wrote:
Should I add headers as the one in mathcomp, as the documentation suggest?
https://github.com/math-comp/math-comp/wiki/How-to-document
— Reply to this email directly, view it on GitHub https://github.com/SSProve/ssprove/pull/57#issuecomment-2774725339, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTVBHLAVAX4UT5IWU732XTO7HAVCNFSM6AAAAAB2ELVP2CVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDONZUG4ZDKMZTHE . You are receiving this because you commented.Message ID: @.***> [image: ErVinuelas]ErVinuelas left a comment (SSProve/ssprove#57) https://github.com/SSProve/ssprove/pull/57#issuecomment-2774725339
Should I add headers as the one in mathcomp, as the documentation suggest?
https://github.com/math-comp/math-comp/wiki/How-to-document
— Reply to this email directly, view it on GitHub https://github.com/SSProve/ssprove/pull/57#issuecomment-2774725339, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTVBHLAVAX4UT5IWU732XTO7HAVCNFSM6AAAAAB2ELVP2CVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDONZUG4ZDKMZTHE . You are receiving this because you commented.Message ID: @.***>