Documentation

Batteries.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
    instance LazyList.instInhabited {α : Type u_1} :
    Equations
    • LazyList.instInhabited = { 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
        @[irreducible]
        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
          • x.headI = match x with | LazyList.nil => default | LazyList.cons h tl => h
          Instances For
            def LazyList.tail {α : Type u_1} :
            LazyList αLazyList α

            Removes the first element of the lazy list.

            Equations
            • x.tail = match x with | LazyList.nil => LazyList.nil | LazyList.cons hd t => t.get
            Instances For
              @[irreducible]
              def LazyList.append {α : Type u_1} :
              LazyList αThunk (LazyList α)LazyList α

              Appends two lazy lists.

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

                Maps a function over a lazy list.

                Equations
                Instances For
                  @[irreducible]
                  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
                      @[irreducible]
                      def LazyList.join {α : Type u_1} :

                      The monadic join operation for lazy lists.

                      Equations
                      • LazyList.nil.join = LazyList.nil
                      • (LazyList.cons h t).join = h.append { fn := fun (x : Unit) => t.get.join }
                      Instances For
                        def LazyList.take {α : Type u_1} :
                        NatLazyList αList α

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

                        Equations
                        Instances For
                          @[irreducible]
                          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