DECapitalize

[jcommelin]

We should have a function that decapitalizes initial clusters of uppercase letters, as that's how the naming convention works.

See also: https://github.com/leanprover-community/mathport/pull/219/files/c1690c803df3b33db0fae93d1e911245a78444fd#r1081895321

[rwbarton]

I think the actual algorithm here should be:

• If the name begins with three or more capital letters followed by non-capital letters, then decapitalize all but the last of the leading capital letters (e.g. GCDMonoid -> gcdMonoid).
• Otherwise, decapitalize all of the leading string of capital letters (e.g. SMul -> smul, XYZ -> xyz -- I don't think we have any names like that yet, but we might in the future).

[rwbarton]

Note that hAdd etc. from core do not follow this convention.