Zulip Chat Archive
Stream: PR reviews
Topic: chore: deprecate unused MLList material
Kim Morrison (Sep 05 2024 at 03:52):
This is code that I wrote about the MLList type, that is not used, or in my opinion useful, anywhere in Mathlib.
Last updated: May 02 2025 at 03:31 UTC