Why does `aux_def` require visibility?

Stream: lean4

[Thomas Murrills]

aux_def requires explicit visibility (e.g. private aux_def or public aux_def), but I'm not sure why.

To #xy, I'm dealing with a metaprogram which uses a macro for aux_def (here, mathlib's notation3), and wondering if it's appropriate to infer the visibility to use for aux_def by asking for isPrivateName (← getDeclNGen).namePrefix. (See #32749.) But this makes me wonder if there's a reason aux_def doesn't do this by itself, and therefore a reason I shouldn't. :)

[Thomas Murrills]

Re: #xy: I think I've realized my mistake there. It seems that commands which create meta defs like syntax and macro_rules uniformly use local to indicate private visibility; likewise, my sense is that we should use private aux_def if the attrKind is local, and public otherwise.

I suppose this explains why we want to insist on the metaprogrammer passing in the visibility explicitly?

[Sebastian Ullrich]

Yes, exactly