Lean 4.22 (to be released in early August) will ship with the first version of the new iterators library, allowing for efficient streaming, combining and collecting of data. This library was designed and implemented by Paul, and he has put a lot of thought into making sure that iterators are compiled into efficient code (like in Rust), and he has worked even harder to ensure that it’s easy to prove things about iterators (even when iterating monadically).
