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: Feb 28 2026 at 14:05 UTC