Lazy lists #

The type LazyList α is a lazy list with elements of type α. In the VM, these are potentially infinite lists where all elements after the first are computed on-demand. (This is only useful for execution in the VM, logically we can prove that LazyList α is isomorphic to List α.)

inductive LazyList (α : Type u) :

Lazy list. All elements (except the first) are computed lazily.

Instances For
    • LazyList.instInhabitedLazyList = { default := LazyList.nil }
    def LazyList.singleton {α : Type u} :
    αLazyList α

    The singleton lazy list.

    def LazyList.ofList {α : Type u} :
    List αLazyList α

    Constructs a lazy list from a list.

    def LazyList.toList {α : Type u} :
    LazyList αList α

    Converts a lazy list to a list. If the lazy list is infinite, then this function does not terminate.

    def LazyList.headI {α : Type u} [inst : Inhabited α] :
    LazyList αα

    Returns the first element of the lazy list, or default if the lazy list is empty.

    def LazyList.tail {α : Type u} :
    LazyList αLazyList α

    Removes the first element of the lazy list.

    def LazyList.append {α : Type u} :
    LazyList αThunk (LazyList α)LazyList α

    Appends two lazy lists.

    def {α : Type u} {β : Type v} (f : αβ) :
    LazyList αLazyList β

    Maps a function over a lazy list.

    def LazyList.map₂ {α : Type u} {β : Type v} {δ : Type w} (f : αβδ) :
    LazyList αLazyList βLazyList δ

    Maps a binary function over two lazy list. Like, the result is only as long as the smaller input.

    def {α : Type u} {β : Type v} :
    LazyList αLazyList βLazyList (α × β)

    Zips two lazy lists.

    def LazyList.join {α : Type u} :

    The monadic join operation for lazy lists.

    def LazyList.for {α : Type u} {β : Type v} (l : LazyList α) (f : αβ) :

    Maps a function over a lazy list. Same as, but with swapped arguments.

    def LazyList.approx {α : Type u} :
    NatLazyList αList α

    The list containing the first n elements of a lazy list.

    def LazyList.filter {α : Type u} (p : αProp) [inst : DecidablePred p] :
    LazyList αLazyList α

    The lazy list of all elements satisfying the predicate. If the lazy list is infinite and none of the elements satisfy the predicate, then this function will not terminate.

    def LazyList.nth {α : Type u} :
    LazyList αNatOption α

    The nth element of a lazy list as an option (like list.nth).

    unsafe def LazyList.iterates {α : Type u} (f : αα) :
    αLazyList α

    The infinite lazy list [x, f x, f (f x), ...] of iterates of a function. This definition is meta because it creates an infinite list.

    unsafe def LazyList.iota (i : Nat) :

    The infinite lazy list [i, i+1, i+2, ...]