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

Estimated changes

deleted def F
deleted def append
deleted def half_or_fail
deleted def l1
deleted def l2
deleted def ll