Pierre Jouvelot (Mar 06 2022 at 21:03): Pierre Jouvelot (Mar 06 2022 at 21:03):Just out of curiosity, what is the logic behind the use of the A/B/C letters in lemmas such as addnBCA? There must be one, but it is not right away obvious to me. A similar question arises with A/B and subn... names. Thanks.
Karl Palmskog (Mar 06 2022 at 21:25):see here: https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md#where
Karl Palmskog (Mar 06 2022 at 21:27):we managed to get quite good naming prediction rates from theorem statements with neural machine learning, which probably says something about the MathComp naming schemes being quite robust
Last updated: Jan 29 2023 at 19:02 UTC