namespacing mathport syntax?

Stream: mathlib4

[Thomas Murrills]

Do namespaces matter for mathport syntax? For example, the syntax for mono (attribute and tactic is

...
namespace Tactic

syntax mono.side := &"left" <|> &"right" <|> &"both" -- Lean.Parser.Tactic.mono.side

syntax (name := mono) "mono" "*"? (ppSpace mono.side)?
  (" with " (colGt term),+)? (" using " (colGt simpArg),+)? : tactic -- Lean.Parser.Tactic.mono

end Tactic
...
namespace Attr

syntax (name := mono) "mono" (ppSpace Tactic.mono.side)? : attr -- Lean.Parser.Attr.mono

end Attr
...

Do these namespaces need to match when implemented somehow? So far it seems like they haven't needed to (e.g. many syntax names for tactic are in Mathlib.Tactic).

For this specific case, the tactic file imports the attribute file, so it's more natural to put mono.side in the attribute file instead of the tactic file. So, there's also the question of whether the mono in mono.side needs to remain the Tactic.mono mono instead of the Attr.mono mono.

[Gabriel Ebner]

No, the namespaces are almost completely irrelevant except for 1) name clashes, and 2) if someone writes TSyntax ``mono (then you need to open the right namespace).