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).