Name.getString

Stream: mathlib4

[Kim Morrison]

Currently Mathlib has Name.getString, which is poorly named. It in fact takes the last component of the name, and makes a best effort to represent this as a string:

/-- Get the last field of a name as a string.
Doesn't raise an error when the last component is a numeric field. -/
def getString : Name → String
  | .str _ s => s
  | .num _ n => toString n
  | .anonymous => ""

It is only used in the implementation of @[simps] and @[to_additive]. I'd like to rename it.

[Kim Morrison]

Name.lastComponentAsString? #12891

[Kim Morrison]

or just Name.lastAsString?