Functions I found implementing this function or a variant:

• Lean.Elab.mkDeclName
• Lean.Elab.Command.elabSyntax doesn't use the function, but should (see fix: resolve _root_ in macro, syntax, elab #2239). That PR introduces 4 reimplementations of the function
• Lean.Elab.Term.elabWithDeclName should also be using the function (basically every use of (← getCurrNamespace) ++ id is suspect)

I'm wondering if removing the _root_ prefix from the rhs is a bit excessive. Maybe the user should decide whether to remove it afterwards.

I think the function should be specced to always remove the _root_ prefix and return a fully qualified name. The use code can put _root_ on the front if needed. It shouldn't add the _root_ always because _root_ prefixed names aren't valid fully qualified names, they are a directive to whatever is processing the name to (suppress additional namespaces and) remove the _root_ before using the name, so you would only want to use that when putting the name back into syntax or similar to be re-processed.

Should it then also remove _root_ from the namespace prefix, or just assume that it is a proper namespace?

Namespaces can't have _root_.

So it is fine as is, with a small edit to the docs?

Fixed!

std4#184 has evolved into std4#200, which doesn't currently use this function. I'm not unilaterally closing this since this PR could be useful for other purposes.

Thanks for the PR. At this point I think it's fair to say it will not be merged by itself but might still be included in other PRs where it makes sense.