Commit 2024-07-15 23:26 8b657060
View on Github →chore: bump dependencies (upstream LazyList) (#14778)
Also adjusts names arguments to LawfulMonad.mk'
to match their actual order.
For some reason the motive now has to be specified explicitly.
I'm not really interested in understanding why, however, because this file, in Batteries and Mathlib is about to be deprecated on the grounds that LazyList is not currently being used, is not actually useful in practice without VM support (it was ported from Mathlib3, where it did have such support), and MLList supplies much of the functionality.