Connecting `Lean.NamePart` to `Lean.Name`

Stream: lean4

[Eric Wieser]

Would the following be a welcome addition to Lean core, perhaps deprecating docs#Lean.Name.components at the same time?

/-- Reversed version of `Lean.Name.parts`. -/
def Lean.Name.partsRev : Name → List Lean.NamePart
  | anonymous => []
  | str n s   => .str s :: partsRev n
  | num n v   => .num v :: partsRev n

/-- The dot-separated parts of a name.

Like `Lean.Name.components`, but the type guarantees each piece is a single component. -/
def Lean.Name.parts (n : Name) : List Lean.NamePart :=
  n.partsRev.reverse

/-- Appending a part to the end of an existing name is a natural operation. -/
instance : HAppend Lean.Name Lean.NamePart Lean.Name where
  hAppend
  | nm, .str s => .str nm s
  | nm, .num n => .num nm n

/-- Build a name from its parts. -/
def Lean.Name.ofParts (cs : List NamePart) : Name :=
  cs.foldl (init := .anonymous) fun n p => n ++ (p : NamePart)

/-- A standalone part can be treated as a name. -/
abbrev Lean.NamePart.toName (n : NamePart) : Name := Name.anonymous ++ n