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.

Estimated changes

deleted theorem LazyList.append_assoc
deleted theorem LazyList.append_bind
deleted theorem LazyList.append_nil
deleted def LazyList.attach
deleted def LazyList.find
deleted theorem LazyList.forall_mem_cons
deleted def LazyList.init
deleted def LazyList.interleave
deleted theorem LazyList.mem_cons
deleted theorem LazyList.mem_nil
deleted def LazyList.mfirst
deleted def LazyList.pmap
deleted def LazyList.reverse