add protected after the fact? #740
Description
We need a mechanism to add protected, or otherwise to tell alias to create protected declarations.
There is an example in Mathlib/Algebra/GroupWithZero/Units/Basic.lean.
{{ message }}
We need a mechanism to add protected, or otherwise to tell alias to create protected declarations.
There is an example in Mathlib/Algebra/GroupWithZero/Units/Basic.lean.