to_additive and public/private, expose/no_expose

Stream: mathlib4

[Jireh Loreaux]

Does to_additive currently handle public and private and expose and no_expose appropriately when they are listed on individual declarations?

[Bhavik Mehta]

I'm not sure if this answers your question, but #metaprogramming / tactics > to_additive and module system is likely relevant

[Jireh Loreaux]

Thanks, but I don't think this answers the question.

[Jireh Loreaux]

Basically, if one does:

@[to_additive]
private def ...

is the additive version also private? Likewise for no_expose, etc.

[Floris van Doorn]

This has to be tested. to_additive uses docs#Lean.addDecl (with forceExpose := false) and I believe this is then added to the public scope iff you're in a public section.

If @[to_additive] private def ... is a macro for

private section
@[to_additive]
def ...

(I don't know if it is), then this should work correctly.

[Floris van Doorn]

never mind, @[to_additive] deals with both of those things:
private
expose