protected to_additive

Stream: general

[Johan Commelin]

When I mark a multiplicative lemma as protected and I generate the additive analogue with to_additive, then the protected label is not carried over. Is this a known bug?

[Simon Hudon]

I don't think there's any available meta programming feature to deal with protected / private