Custom attribute that also adds `extern`

Stream: lean4

[Arthur Paulino]

I'm trying to create a custom attribute that, besides serving as our own tag, also adds the extern tag to a declaration.
This is my current attempt, but turns out this ends up not adding the extern tag to declarations.
Is it possible to do so? Thanks in advance!

[Arthur Paulino]

If this cannot be done, we can get away with using two tags, but it would be more comfortable if a single tag could be used.

[Joe Hendrix]

@Arthur Paulino I'm curious about this to.
I did notice the condition env.isProjectionFn declName || env.isConstructor declName evaluates to false, and when I just remove the check, I get a kernel panic in addExtern. Maybe there's a different way to attach an attribute to a declaration in the environment?