weird `toAdditive` name

Stream: mathlib4

[Sébastien Gouëzel]

The additivization of docs#ContinuousMul.measurableMul is, as you may expect, docs#ContinuousAdd.measurableAdd. The additivization of docs#ContinuousMul.measurableMul₂ is, more surprisingly, docs#ContinuousAdd.measurableMul₂. I could tweak it by hand to give it the right name, but I'd rather understand what is going on here in a more principled way...

[Michael Rothgang]

CC @Floris van Doorn

[Yaël Dillies]

You need to add an entry to docs#ToAdditive.nameDict

[Sébastien Gouëzel]

An entry like what? Mul is normally additivized to Add. The problem is the suffix ₂ here. Adding an entry for each suffix doesn't look like an optimal strategy...

[Michael Rothgang]

Should to_additive be modified to split off superscript suffixes, try to additivise the name and rejoin them?

[Yaël Dillies]

Sébastien Gouëzel said:

Adding an entry for each suffix doesn't look like an optimal strategy...

There are only 10 digit and 17 letter subscripts after all... :grinning:

[Jz Pan]

Yaël Dillies said:

Sébastien Gouëzel said:

Adding an entry for each suffix doesn't look like an optimal strategy...

There are only 10 digit and 17 letter subscripts after all... :grinning:

But digits can be combined for numbers

[Damiano Testa]

Or maybe nameDict should be taught to split names at sub/super scripts.

[Floris van Doorn]

As others have said, the easiest is indeed to teach docs#String.splitCase that all subscript/superscript characters are separators between word parts. Currently we only consider _ as a separator, but I think it's fine to also separate on all subscript digits (or all sub/superscript letters/digits - changing ᵐᵘˡ to ᵃᵈᵈ can be outside the scope of to_additive).