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

[Fernando Chu]

Is there any workaround this?

[Michael Rothgang]

This also came up in the discussion of differential geometry elaborators - so let me second "this would be great to have".

[Michael Rothgang]

That thread is here #mathlib4 > Differential geometry elaborators experiment