Commit 2024-05-30 11:57 a5844cab

View on Github →

chore: add deprecation dates for nat_cast and int_cast lemmas (#13368) Deprecations have been forgotten in #11486. We add them in this PR. Methodology: start from the last commit of #11486, use the script by @adomani in https://github.com/leanprover-community/mathlib4/pull/10185#issuecomment-1925481325 to generate deprecation aliases (I am also adding an updated version of the script in a comment below) and commit. Then cherry pick this last commit on master and fix whatever has changed in between. This is not perfect as declarations which have been moved since #11486 won't get their deprecated alias, but this should be good enough.

Estimated changes