Commit 2022-11-25 16:23 e40e2a78
View on Github →feat: improve toAdditive.guessName (#715)
- The heuristic to split names did it wrong on a long sequence of capital letters. The new heuristic is to have a sequence of "white-listed" names that only consist of capital letters (currently
["LE", "LT", "WF"]). This new heuristic correctly splitsZeroLEHAddandHSMul - translate
[h]powto[h]smul(see #706). I believe Mathlib4 never used the previous automatic translationpow -> nsmul(I used regex@\[to_additive\]\n?.*(_p|P| p)owto search). Since capitalization goes wrong in this case, add some cases infixAbbreviationto fix it. - Fix all places where the capitalization
Smulwas used instead ofSMul.