Zulip Chat Archive
Stream: maths
Topic: deprecated
Dean Young (Apr 03 2024 at 05:00):
"https://leanprover-community.github.io/mathlib4_docs/Mathlib/"
Is "deprecated" supposed to be "depreciated"? Why is it deprecated?
Yaël Dillies (Apr 03 2024 at 05:42):
See Usage notes here
Eric Wieser (Apr 10 2024 at 06:54):
And also https://www.merriam-webster.com/dictionary/deprecate
Last updated: May 02 2025 at 03:31 UTC