leanprover-community/mathlib4
Make `scripts/add_deprecations.sh` support additivised declarations
開放
#38,550 建立於 2026年4月26日
enhancementgood first issue
倉庫指標
- 星標
- (3,869 顆星)
- PR 合併指標
- (30 天內沒有已合併 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).