chore: clarify docstring

leanprover · Jul 21, 2023 · d358c17 · d358c17
1 parent ab4cce2
commit d358c17
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/src/Lean/Data/OpenDecl.lean b/src/Lean/Data/OpenDecl.lean
@@ -28,13 +28,15 @@ def rootNamespace := `_root_
 def removeRoot (n : Name) : Name :=
   n.replacePrefix rootNamespace Name.anonymous
 
-/-- Adds namespace prefix unless in root namespace, when it just removes `_root_`.
+/-- `addNamespaceUnlessRoot ns n` adds namespace `ns` prefix unless `n` has a `_root_` prefix.
+If `n` has a `_root_` prefix then it is removed and `ns` is not added. The end result is a fully
+qualified name assuming that `ns` is a proper namespace prefix.
 ```
 addNamespaceUnlessRoot `a.b `c.d = `a.b.c.d
 addNamespaceUnlessRoot `a.b `_root_.c.d = `c.d
 ```
 -/
-abbrev addNamespaceUnlessRoot (ns : Name) (n : Name) : Name :=
+def addNamespaceUnlessRoot (ns : Name) (n : Name) : Name :=
   if rootNamespace.isPrefixOf n then removeRoot n else ns ++ n
 
 end Lean