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 splitsZeroLEHAdd
andHSMul
- translate
[h]pow
to[h]smul
(see #706). I believe Mathlib4 never used the previous automatic translationpow -> nsmul
(I used regex@\[to_additive\]\n?.*(_p|P| p)ow
to search). Since capitalization goes wrong in this case, add some cases infixAbbreviation
to fix it. - Fix all places where the capitalization
Smul
was used instead ofSMul
.