Documentation

Std.Data.LazyList

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
    Equations
    • LazyList.instInhabitedLazyList = { default := LazyList.nil }
    def LazyList.singleton {α : Type u_1} :
    αLazyList α

    The singleton lazy list.

    Equations
    Instances For
      def LazyList.ofList {α : Type u_1} :
      List αLazyList α

      Constructs a lazy list from a list.

      Equations
      Instances For
        def LazyList.toList {α : Type u_1} :
        LazyList αList α

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

        Equations
        Instances For
          def LazyList.headI {α : Type u_1} [Inhabited α] :
          LazyList αα

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

          Equations
          Instances For
            def LazyList.tail {α : Type u_1} :
            LazyList αLazyList α

            Removes the first element of the lazy list.

            Equations
            Instances For
              def LazyList.append {α : Type u_1} :
              LazyList αThunk (LazyList α)LazyList α

              Appends two lazy lists.

              Equations
              Instances For
                def LazyList.map {α : Type u_1} {β : Type u_2} (f : αβ) :
                LazyList αLazyList β

                Maps a function over a lazy list.

                Equations
                Instances For
                  def LazyList.map₂ {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : αβδ) :
                  LazyList αLazyList βLazyList δ

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

                  Equations
                  Instances For
                    def LazyList.zip {α : Type u_1} {β : Type u_2} :
                    LazyList αLazyList βLazyList (α × β)

                    Zips two lazy lists.

                    Equations
                    Instances For
                      def LazyList.join {α : Type u_1} :

                      The monadic join operation for lazy lists.

                      Equations
                      Instances For
                        def LazyList.take {α : Type u_1} :
                        NatLazyList αList α

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

                        Equations
                        Instances For
                          def LazyList.filter {α : Type u_1} (p : αProp) [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.

                          Equations
                          Instances For
                            def LazyList.get? {α : Type u_1} :
                            LazyList αNatOption α

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

                            Equations
                            Instances For
                              partial def LazyList.iterates {α : Type u_1} (f : αα) :
                              αLazyList α

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

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

                              Equations
                              Instances For