Lean4
/-- `scoped[NS]` is similar to the `scoped` modifier on attributes and notations,
but it scopes the syntax in the specified namespace instead of the current namespace.
```
scoped[Matrix] postfix:1024 "ᵀ" => Matrix.transpose
-- declares `ᵀ` as a notation for matrix transposition
-- which is only accessible if you `open Matrix` or `open scoped Matrix`.
namespace Nat
scoped[Nat.Count] attribute [instance] CountSet.fintype
-- make the definition Nat.CountSet.fintype an instance,
-- but only if `Nat.Count` is open
```
-/
@[command_parser 1000]
public meta def scopedNS : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.scopedNS 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.unary✝ `optional (ParserDescr.const✝ `docComment))
(ParserDescr.unary✝ `optional (ParserDescr.parser✝ `Lean.Parser.Term.attributes)))
(ParserDescr.symbol✝ "scoped"))
(ParserDescr.symbol✝ "["))
(ParserDescr.const✝ `ident))
(ParserDescr.symbol✝ "] "))
(ParserDescr.cat✝ `command 0))
