Zulip Chat Archive
Stream: mathlib4
Topic: to_additive and deprecated alias
Yury G. Kudryashov (Oct 06 2024 at 22:19):
What's the right way to create a deprecated alias for a lemma with to_additive?
Floris van Doorn (Oct 06 2024 at 22:33):
@[to_additive (attr := deprecated (since := "2024-10-07"))]
Yury G. Kudryashov (Oct 06 2024 at 22:36):
In https://github.com/leanprover-community/mathlib4/actions/runs/11204670478/job/31143326980?pr=17472 (see code) it fails to add a docstring.
Yury G. Kudryashov (Oct 06 2024 at 22:37):
I tried to split it into parts in the latest commit in #17472, not sure if it works.
Yury G. Kudryashov (Oct 06 2024 at 22:37):
(and it looks worse)
Floris van Doorn (Oct 07 2024 at 10:35):
Oh, I see. to_additive indeed doesn't copy docstrings by itself...
Yury G. Kudryashov (Oct 07 2024 at 12:36):
I "fixed" by using @[deprecated] alias on both defs, then adding to_additive existing while turning off a linter.
Yury G. Kudryashov (Oct 07 2024 at 12:37):
Yury G. Kudryashov (Oct 09 2024 at 14:52):
One more issue: while @[deprecated] alias name := other_name generates @[deprecated other_name] theorem name := _, @[to_additive (attr := deprecated)] creates a nameless deprecation.
Yury G. Kudryashov (Oct 09 2024 at 14:53):
So, if someone uses the lemma, they don't see the preferred name in the warning.
Last updated: May 02 2025 at 03:31 UTC