Zulip Chat Archive
Stream: lean4
Topic: No warning on deprecated local instances
Robin Carlier (Jun 22 2025 at 11:27):
In this file in a PR, line 150, there is
attribute [local instance] small_quot_of_hasColimit
This identifier is in fact deprecated (l.109 just above).
Is this normal that this does not produce a warning?
Last updated: Dec 20 2025 at 21:32 UTC