scoped[NS] doesn't work with syntax

Stream: mathlib4

[Yaël Dillies]

Looks like one can't use the scoped[NS] syntax combo:

import Mathlib.Data.Set.Defs
import Mathlib.Tactic.ScopedNS

scoped[Set] syntax (name := stab) "Stab " term:arg : term
-- elaboration function for 'Mathlib.Tactic.scopedNS' has not been implemented

[Yaël Dillies]

Is this known?

[Mario Carneiro]

it was originally designed for lean 3 after all

[Yaël Dillies]

Should we fix it? or are you implying we should remove the notation altogether?

[Mario Carneiro]

#18230