local attribute [ext] only works once

Stream: general

[Eric Wieser]

What can we do about this?

import tactic.ext

structure foo :=
(x : int)
(y : int)

section
local attribute [ext] foo  -- ok

end

section
local attribute [ext] foo  -- fails, `foo.ext` already exists

end

Can we forbid ext being used locally on structures?

[Floris van Doorn]

Yeah, forbidding it as a local attribute makes sense if it generates new declarations. This is also done in other attributes