More Operations on Lazy Lists

Andrei Popescu 📧 and Jamie Wright 📧

May 24, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We formalize some operations and reasoning infrastructure on lazy (coinductive) lists. The operations include: building a lazy list from a function on naturals and an extended natural indicating the intended domain, take-until and drop-until (which are variations of take-while and drop-while), splitting a lazy list into a lazy list of lists with cut points being those elements that satisfy a predicate, and filtermap. The reasoning infrastructure includes: a variation of the corecursion combinator, multi-step (list-based) coinduction for lazy-list equality, and a criterion for the filtermapped equality of two lazy lists.


BSD License


Session More_LazyLists

Depends on

Used by