Zulip Chat Archive
Stream: lean4
Topic: can the `deprecated` attribute set `linter.deprecated false`
Kim Morrison (May 09 2024 at 01:27):
It would be nice if deprecation warnings were turned off inside declarations marked @[deprecated]. Is this possible? If so, PR very welcome. :-)
Last updated: May 02 2025 at 03:31 UTC