Documentation

Batteries.Data.DList.Basic

structure Batteries.DList (α : Type u) :

A difference List is a Function that, given a List, returns the original contents of the difference List prepended to the given List. This structure supports O(1) append and push operations on lists, making it useful for append-heavy uses such as logging and pretty printing.

  • apply : List αList α

    "Run" a DList by appending it on the right by a List α to get another List α.

  • invariant : ∀ (l : List α), self.apply l = self.apply [] ++ l

    The apply function of a DList is completely determined by the list apply [].

Instances For
    theorem Batteries.DList.invariant {α : Type u} (self : Batteries.DList α) (l : List α) :
    self.apply l = self.apply [] ++ l

    The apply function of a DList is completely determined by the list apply [].

    O(1) (apply is O(|l|)). Convert a List α into a DList α.

    Equations
    Instances For

      O(1) (apply is O(1)). Return an empty DList α.

      Equations
      • Batteries.DList.empty = { apply := id, invariant := }
      Instances For
        Equations
        • Batteries.DList.instEmptyCollection = { emptyCollection := Batteries.DList.empty }
        Equations
        • Batteries.DList.instInhabited = { default := Batteries.DList.empty }

        O(apply()). Convert a DList α into a List α by running the apply function.

        Equations
        • { apply := f, invariant := invariant }.toList = f []
        Instances For

          O(1) (apply is O(1)). A DList α corresponding to the list [a].

          Equations
          Instances For

            O(1) (apply is O(1)). Prepend a on a DList α.

            Equations
            Instances For

              O(1) (apply is O(1)). Append two DList α.

              Equations
              • { apply := f, invariant := h₁ }.append { apply := g, invariant := h₂ } = { apply := f g, invariant := }
              Instances For

                O(1) (apply is O(1)). Append an element at the end of a DList α.

                Equations
                • { apply := f, invariant := h }.push x = { apply := fun (t : List α) => f (x :: t), invariant := }
                Instances For
                  Equations
                  • Batteries.DList.instAppend = { append := Batteries.DList.append }

                  Convert a lazily-evaluated List to a DList

                  Equations
                  Instances For
                    @[deprecated Batteries.DList.ofThunk]

                    Alias of Batteries.DList.ofThunk.


                    Convert a lazily-evaluated List to a DList

                    Equations
                    Instances For

                      Concatenates a list of difference lists to form a single difference list. Similar to List.join.

                      Equations
                      Instances For