chore: backward.privateInPublic.warn and attrs

Author: Kha

src/Lean/Attributes.lean

@@ -148,11 +148,14 @@ def throwAttrDeclNotOfExpectedType (attrName declName : Name) (givenType expecte
   throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` has type{indentExpr givenType}\n\
     but `[{attrName}]` can only be added to declarations of type{indentExpr expectedType}"
 
-def ensureAttrDeclIsPublic [MonadEnv m] (attrName declName : Name) (attrKind : AttributeKind) : m Unit := do
-  if (← getEnv).header.isModule && attrKind != .local && !((← getEnv).setExporting true).contains declName then
-    throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be public"
-
-def ensureAttrDeclIsMeta [MonadEnv m] (attrName declName : Name) (attrKind : AttributeKind) : m Unit := do
+def ensureAttrDeclIsPublic (attrName declName : Name) (attrKind : AttributeKind) : AttrM Unit := do
+  if (← getEnv).header.isModule && attrKind != .local then
+    withExporting do
+      checkPrivateInPublic declName
+      if !(← hasConst declName) then
+        throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be public"
+
+def ensureAttrDeclIsMeta (attrName declName : Name) (attrKind : AttributeKind) : AttrM Unit := do
   if (← getEnv).header.isModule && !isMeta (← getEnv) declName then
     throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be marked as `meta`"
   -- Make sure attributed decls can't refer to private meta imports, which is already checked for