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

Estimated changes