Scoped attribute

Stream: mathlib4

[Frédéric Dupuis]

In #1188, there is a scoped attribute being defined:

scoped[Pointwise] attribute [instance] Set.hasOne Set.hasZero

This is apparently not implemented yet, I get the error:

expected 'binder_predicate', 'elab', 'elab_rules', 'infix', 'infixl', 'infixr', 'instance', 'macro', 'macro_rules', 'notation', 'notation3', 'postfix', 'prefix', 'syntax' or 'unif_hint'

Should I just wait for this to get fixed?

[Patrick Massot]

The situation definitely improves if you add import Mathlib.Tactic.ScopedNS at top. However Lean still complains about scoped attribute not being implemented despite https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/ScopedNS.lean#L53 @Mario Carneiro

[Patrick Massot]

The error message is simply

elaboration function for 'Mathlib.Tactic.scopedNS' has not been implemented

[Patrick Massot]

on a line such as scoped[Pointwise] attribute [instance] Set.hasInv Set.hasNeg

[Mario Carneiro]

I don't see any obvious reason for that. I assume the line has no doc comment or attributes?

[Patrick Massot]

MWE:

import Mathlib.Tactic.ScopedNS

theorem foo : 1 + 1 = 2 := rfl

scoped[Nat] attribute [simp] foo

[Patrick Massot]

This is using mathlib4 70c3e2a60de1a253fd835104382304384c3b14ad

[Patrick Massot]

from four days ago.

[Mario Carneiro]

This appears to be a bug in syntax match itself. Reported as lean4#2005

[Patrick Massot]

Thanks a lot for investigating this!