How to deal with conflicting namespaces

Stream: mathlib4

[Praneeth Kolichala]

In !4#2360, when Nat.Primrec' is opened, the name Nat.Primrec conflicts with Primrec. I guess in Lean 3, when you wrote Primrec when only Nat.Primrec was open, it would refer to Primrec from the root namespace, but now, Primrec refers to Nat.Primrec, and we need to write _root_.Primrec to explicitly refer to the root.

Does this indicate that some renaming is in order, or is writing _root_.Primrec everywhere in that namespace OK?

[Jireh Loreaux]

I would be tempted instead to add protected to Nat.Primrec (and maybe Nat.Primrec').

[Jireh Loreaux]

This doesn't require any renaming, and arguably nat.primrec should have been protected in Lean 3.