Lean4
@[macro Mathlib.Tactic.scopedNS]
public meta def _aux_Mathlib_Tactic_ScopedNS___macroRules_Mathlib_Tactic_scopedNS_1 : Macro✝ := fun
| `($[$doc]?$(attr)?scoped[$ns] notation$(prec)?$(n)?$(prio)? $sym* => $t) =>
`(with_weak_namespace
$(mkIdentFrom ns <| rootNamespace ++ ns.getId)$[$doc]?$(attr)?scoped notation$(prec)?$(n)?$(prio)? $sym* => $t)
| `($[$doc]?$(attr)?scoped[$ns] $mk:prefix$prec$(n)?$(prio)? $sym => $t) =>
`(with_weak_namespace
$(mkIdentFrom ns <| rootNamespace ++ ns.getId)$[$doc]?$(attr)?scoped $mk:prefix$prec$(n)?$(prio)? $sym => $t)
| `($[$doc]?$(attr)?scoped[$ns] $mk:infix$prec$(n)?$(prio)? $sym => $t) =>
`(with_weak_namespace
$(mkIdentFrom ns <| rootNamespace ++ ns.getId)$[$doc]?$(attr)?scoped $mk:infix$prec$(n)?$(prio)? $sym => $t)
| `($[$doc]?$(attr)?scoped[$ns] $mk:infixl$prec$(n)?$(prio)? $sym => $t) =>
`(with_weak_namespace
$(mkIdentFrom ns <| rootNamespace ++ ns.getId)$[$doc]?$(attr)?scoped $mk:infixl$prec$(n)?$(prio)? $sym => $t)
| `($[$doc]?$(attr)?scoped[$ns] $mk:infixr$prec$(n)?$(prio)? $sym => $t) =>
`(with_weak_namespace
$(mkIdentFrom ns <| rootNamespace ++ ns.getId)$[$doc]?$(attr)?scoped $mk:infixr$prec$(n)?$(prio)? $sym => $t)
| `($[$doc]?$(attr)?scoped[$ns] $mk:postfix$prec$(n)?$(prio)? $sym => $t) =>
`(with_weak_namespace
$(mkIdentFrom ns <| rootNamespace ++ ns.getId)$[$doc]?$(attr)?scoped $mk:postfix$prec$(n)?$(prio)? $sym => $t)
| `(scoped[$ns] attribute [$[$attr:attr],*] $ids*) =>
`(with_weak_namespace $(mkIdentFrom ns <| rootNamespace ++ ns.getId)attribute [$[scoped $attr:attr],*] $ids*)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
