Commit 2024-07-23 23:19 54e631e2
View on Github →chore: update Batteries and deprecate LazyList (#15040)
LazyList was deprecated in Batteries (with an indication to use MLList instead). The uses in Mathlib were trivial, as they were immediately forced to a List anyway. This PR deprecates the code about LazyList, and replaces the lazy-but-not-really code with strict versions.