update test output

Move the `scoped[NS]` syntax definition from `Lean.Elab.Command.ScopedNamespace`
to `Init.NotationExtra` so it's available without explicit imports.

The macro implementation remains in `Lean.Elab.Command.ScopedNamespace` but now
converts the new `scopedNSAttrs` syntax type to `Term.attributes` for compatibility
with the output notation commands.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

src/Init/NotationExtra.lean

@@ -357,4 +357,27 @@ meta def insertUnexpander : Lean.PrettyPrinter.Unexpander
   | `($_ $a { $ts:term,* }) => `({$a:term, $ts,*})
   | _ => throw ()
 
+namespace Parser.Command
+
+/-- An attribute instance with optional scoped/local modifier. -/
+syntax scopedNSAttrInstance := attrKind attr
+
+/-- Attributes syntax `@[...]` for scoped namespace commands. -/
+syntax scopedNSAttrs := "@[" sepBy1(scopedNSAttrInstance, ", ") "] "
+
+/--
+Syntax for declaring notations and attributes that are scoped to a specific namespace,
+without being inside that namespace. For example:
+
+```lean
+scoped[Nat] infix:65 " +! " => Nat.add
+```
+
+defines an infix notation that is only available when `Nat` is opened.
+-/
+syntax (name := scopedNS) (docComment)? (scopedNSAttrs)?
+  "scoped" "[" ident "] " command : command
+
+end Parser.Command
+
 end Lean

src/Lean/Elab.lean

@@ -47,6 +47,7 @@ public import Lean.Elab.Mixfix
 public import Lean.Elab.MacroRules
 public import Lean.Elab.BuiltinCommand
 public import Lean.Elab.Command.WithWeakNamespace
+public import Lean.Elab.Command.ScopedNamespace
 public import Lean.Elab.BuiltinEvalCommand
 public import Lean.Elab.RecAppSyntax
 public import Lean.Elab.Eval

src/Lean/Elab/Command/ScopedNamespace.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Daniel Selsam, Gabriel Ebner
+-/
+
+module
+
+prelude
+public import Lean.Elab.Command.WithWeakNamespace
+
+namespace Lean.Elab.Command
+
+private def toTermAttrs (attr : TSyntax `Lean.Parser.Command.scopedNSAttrs) :
+    TSyntax `Lean.Parser.Term.attributes :=
+  ⟨attr.raw.setKind `Lean.Parser.Term.attributes⟩
+
+@[builtin_macro Lean.Parser.Command.scopedNS] def expandScopedNS : Macro
+  | `($[$doc]? $(attr)? scoped[$ns] notation $(prec)? $(n)? $(prio)? $sym* => $t) => do
+    let attr' := attr.map toTermAttrs
+    `(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) => do
+    let attr' := attr.map toTermAttrs
+    `(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) => do
+    let attr' := attr.map toTermAttrs
+    `(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) => do
+    let attr' := attr.map toTermAttrs
+    `(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) => do
+    let attr' := attr.map toTermAttrs
+    `(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) => do
+    let attr' := attr.map toTermAttrs
+    `(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*)
+  | _ => Macro.throwUnsupported
+
+end Lean.Elab.Command

tests/lean/run/scopedNS.lean

@@ -0,0 +1,62 @@
+module
+/-
+Tests for scoping syntax to a specific namespace using `scoped[NS]`
+-/
+
+
+-- Test 1: Scoped notation in a different namespace
+namespace A
+
+scoped[B] postfix:1024 " !" => Nat.succ
+
+end A
+
+-- The notation should be accessible when opening B
+open B
+#guard (5 ! = 6)
+
+-- Test 2: Scoped infix notation
+scoped[Math] infix:65 " ⊕ " => Nat.add
+
+/-- info: 7 -/
+#guard_msgs in
+open Math in
+#eval 3 ⊕ 4
+
+/--
+error: failed to synthesize instance of type class
+  OfNat (Type _) 3
+numerals are polymorphic in Lean, but the numeral `3` cannot be used in a context where the expected type is
+  Type _
+due to the absence of the instance above
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+error: failed to synthesize instance of type class
+  OfNat (Type _) 4
+numerals are polymorphic in Lean, but the numeral `4` cannot be used in a context where the expected type is
+  Type _
+due to the absence of the instance above
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+error: cannot evaluate, types are not computationally relevant
+-/
+#guard_msgs in
+set_option pp.mvars false in
+#eval 3 ⊕ 4
+
+
+-- Test 3: Scoped attribute
+def myInstance : Inhabited Nat := ⟨42⟩
+
+scoped[MyNS] attribute [instance] myInstance
+
+/-- info: 42 -/
+#guard_msgs in
+open MyNS in
+#eval (default : Nat)
+
+/-- info: 0 -/
+#guard_msgs in
+#eval (default : Nat)

tests/lean/versoDocMissing.lean.expected.out

@@ -1 +1 @@
-versoDocMissing.lean:10:0: error: unexpected end of input; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'coinductive', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_error_explanation', 'register_tactic_tag', 'register_try?_tactic', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'
+versoDocMissing.lean:10:0: error: unexpected end of input; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'coinductive', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_error_explanation', 'register_tactic_tag', 'register_try?_tactic', 'scoped', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'