Commit 2024-09-05 04:30 c3e9dfae
View on Github →chore: deprecate unused MLList material, which has moved to a separate repo (#16057) This material is unused in Mathlib, and now exists in a separate repo at https://github.com/semorrison/lean-monadic-list