leanprover-community/mathlib4
Make `scripts/add_deprecations.sh` support additivised declarations
オープン
#38,550 opened on 2026/04/26
enhancementgood first issue
Repository metrics
- Stars
- (3,869 個のスター)
- PR merge metrics
- (30d に merged PR はありません)
説明
Currently, changing
@[to_additive]
lemma foo_mul ...
to
@[to_additive]
lemma bar_mul ...
then running scripts/add_deprecations.sh creates
@[to_additive]
lemma bar_mul ...
@[deprecated ...] alias foo_mul := bar_mul
It should instead create
@[to_additive]
lemma bar_mul ...
@[deprecated ...] alias foo_mul := bar_mul
@[deprecated ...] alias foo_add := bar_add
Note that
@[to_additive (attr := deprecated ...)] alias foo_mul := bar_mul
doesn't work because deprecated loses track of what the deprecated declaration is an alias of (see #19424).