Skip to content

doc: also mention the full syntax for the deprecated attribute #8339

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

grunweg
Copy link
Contributor

@grunweg grunweg commented May 14, 2025

The other day, I wanted to apply the full form (i.e., with both a custom message and a deprecation date) in mathlib and failed to guess the correct order of these two. The attribute doc-string seemed to suggest that combining them was impossible (which was luckily false).

To prevent this from re-occurring, clarify the doc-string by

  • mentioning that a custom message and deprecation date can be combined
  • what the expected order of these two is

The other day, I wanted to apply the full form (i.e., with both a custom
message and a deprecation date) in mathlib and failed to guess the correct
order of these two. The attribute doc-string seemed to suggest that combining
them was impossible (which was luckily false).

To prevent this from re-occurring, clarify the doc-string by
- mentioning that a custom message and deprecation date can be combined
- what the expected order of these two is
@grunweg grunweg changed the title doc: document the full syntax for the deprecation attribute doc: also mention the full syntax for the deprecated attribute May 14, 2025
@grunweg
Copy link
Contributor Author

grunweg commented May 14, 2025

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label May 14, 2025
@grunweg
Copy link
Contributor Author

grunweg commented May 14, 2025

CC @kim-em I presume you might be interested

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 14, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b8c941d39a2a6218769dbaced310fba8f609f7a5 --onto 29cc75531a5a0e8626fa5e96371e7ceb98877782. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-14 20:25:11)

@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label May 28, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-review Waiting for someone to review the PR P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants