Documentation

Batteries.Data.BinomialHeap.Basic

A HeapNode is one of the internal nodes of the binomial heap. It is always a perfect binary tree, with the depth of the tree stored in the Heap. However the interpretation of the two pointers is different: we view the child as going to the first child of this node, and sibling goes to the next sibling of this tree. So it actually encodes a forest where each node has children node.child, node.child.sibling, node.child.sibling.sibling, etc.

Each edge in this forest denotes a le a b relation that has been checked, so the root is smaller than everything else under it.

  • nil {α : Type u} : HeapNode α

    An empty forest, which has depth 0.

  • node {α : Type u} (a : α) (child sibling : HeapNode α) : HeapNode α

    A forest of rank r + 1 consists of a root a, a forest child of rank r elements greater than a, and another forest sibling of rank r.

Instances For
    instance Batteries.BinomialHeap.Imp.instReprHeapNode {α✝ : Type u_1} [Repr α✝] :
    Repr (HeapNode α✝)
    Equations

      The "real size" of the node, counting up how many values of type α are stored. This is O(n) and is intended mainly for specification purposes. For a well formed HeapNode the size is always 2^n - 1 where n is the depth.

      Equations
        Instances For

          A node containing a single element a.

          Equations
            Instances For

              O(log n). The rank, or the number of trees in the forest. It is also the depth of the forest.

              Equations
                Instances For

                  A Heap is the top level structure in a binomial heap. It consists of a forest of HeapNodes with strictly increasing ranks.

                  • nil {α : Type u} : Heap α

                    An empty heap.

                  • cons {α : Type u} (rank : Nat) (val : α) (node : HeapNode α) (next : Heap α) : Heap α

                    A cons node contains a tree of root val, children node and rank rank, and then next which is the rest of the forest.

                  Instances For
                    instance Batteries.BinomialHeap.Imp.instReprHeap {α✝ : Type u_1} [Repr α✝] :
                    Repr (Heap α✝)
                    Equations

                      O(n). The "real size" of the heap, counting up how many values of type α are stored. This is intended mainly for specification purposes. Prefer Heap.size, which is the same for well formed heaps.

                      Equations
                        Instances For

                          O(log n). The number of elements in the heap.

                          Equations
                            Instances For
                              @[inline]

                              O(1). Is the heap empty?

                              Equations
                                Instances For
                                  @[inline]

                                  O(1). The heap containing a single value a.

                                  Equations
                                    Instances For

                                      O(1). Auxiliary for Heap.merge: Is the minimum rank in Heap strictly larger than n?

                                      Equations
                                        Instances For
                                          instance Batteries.BinomialHeap.Imp.instDecidableRankGT {α✝ : Type u_1} {s : Heap α✝} {n : Nat} :
                                          Equations

                                            O(log n). The number of trees in the forest.

                                            Equations
                                              Instances For
                                                @[inline]
                                                def Batteries.BinomialHeap.Imp.combine {α : Type u_1} (le : ααBool) (a₁ a₂ : α) (n₁ n₂ : HeapNode α) :
                                                α × HeapNode α

                                                O(1). Auxiliary for Heap.merge: combines two heap nodes of the same rank into one with the next larger rank.

                                                Equations
                                                  Instances For
                                                    @[irreducible, specialize #[]]
                                                    def Batteries.BinomialHeap.Imp.Heap.merge {α : Type u_1} (le : ααBool) :
                                                    Heap αHeap αHeap α

                                                    Merge two forests of binomial trees. The forests are assumed to be ordered by rank and merge maintains this invariant.

                                                    Equations
                                                      Instances For

                                                        O(log n). Convert a HeapNode to a Heap by reversing the order of the nodes along the sibling spine.

                                                        Equations
                                                          Instances For

                                                            Computes s.toHeap ++ res tail-recursively, assuming n = s.rank.

                                                            Equations
                                                              Instances For
                                                                @[specialize #[]]
                                                                def Batteries.BinomialHeap.Imp.Heap.headD {α : Type u_1} (le : ααBool) (a : α) :
                                                                Heap αα

                                                                O(log n). Get the smallest element in the heap, including the passed in value a.

                                                                Equations
                                                                  Instances For
                                                                    @[inline]
                                                                    def Batteries.BinomialHeap.Imp.Heap.head? {α : Type u_1} (le : ααBool) :
                                                                    Heap αOption α

                                                                    O(log n). Get the smallest element in the heap, if it has an element.

                                                                    Equations
                                                                      Instances For
                                                                        structure Batteries.BinomialHeap.Imp.FindMin (α : Type u_1) :
                                                                        Type u_1

                                                                        The return type of FindMin, which encodes various quantities needed to reconstruct the tree in deleteMin.

                                                                        • before : Heap αHeap α

                                                                          The list of elements prior to the minimum element, encoded as a "difference list".

                                                                        • val : α

                                                                          The minimum element.

                                                                        • node : HeapNode α

                                                                          The children of the minimum element.

                                                                        • next : Heap α

                                                                          The forest after the minimum element.

                                                                        Instances For
                                                                          @[specialize #[]]
                                                                          def Batteries.BinomialHeap.Imp.Heap.findMin {α : Type u_1} (le : ααBool) (k : Heap αHeap α) :
                                                                          Heap αFindMin αFindMin α

                                                                          O(log n). Find the minimum element, and return a data structure FindMin with information needed to reconstruct the rest of the binomial heap.

                                                                          Equations
                                                                            Instances For
                                                                              def Batteries.BinomialHeap.Imp.Heap.deleteMin {α : Type u_1} (le : ααBool) :
                                                                              Heap αOption (α × Heap α)

                                                                              O(log n). Find and remove the the minimum element from the binomial heap.

                                                                              Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def Batteries.BinomialHeap.Imp.Heap.tail? {α : Type u_1} (le : ααBool) (h : Heap α) :

                                                                                  O(log n). Get the tail of the binomial heap after removing the minimum element.

                                                                                  Equations
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      def Batteries.BinomialHeap.Imp.Heap.tail {α : Type u_1} (le : ααBool) (h : Heap α) :
                                                                                      Heap α

                                                                                      O(log n). Remove the minimum element of the heap.

                                                                                      Equations
                                                                                        Instances For
                                                                                          @[irreducible]
                                                                                          theorem Batteries.BinomialHeap.Imp.Heap.realSize_merge {α : Type u_1} (le : ααBool) (s₁ s₂ : Heap α) :
                                                                                          (merge le s₁ s₂).realSize = s₁.realSize + s₂.realSize
                                                                                          theorem Batteries.BinomialHeap.Imp.Heap.realSize_deleteMin {α : Type u_1} {le : ααBool} {a : α} {s' s : Heap α} (eq : deleteMin le s = some (a, s')) :
                                                                                          theorem Batteries.BinomialHeap.Imp.Heap.realSize_tail? {α : Type u_1} {le : ααBool} {s' s : Heap α} :
                                                                                          tail? le s = some s's.realSize = s'.realSize + 1
                                                                                          theorem Batteries.BinomialHeap.Imp.Heap.realSize_tail {α : Type u_1} (le : ααBool) (s : Heap α) :
                                                                                          (tail le s).realSize = s.realSize - 1
                                                                                          @[irreducible, specialize #[]]
                                                                                          def Batteries.BinomialHeap.Imp.Heap.foldM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (le : ααBool) (s : Heap α) (init : β) (f : βαm β) :
                                                                                          m β

                                                                                          O(n log n). Monadic fold over the elements of a heap in increasing order, by repeatedly pulling the minimum element out of the heap.

                                                                                          Equations
                                                                                            Instances For
                                                                                              @[inline]
                                                                                              def Batteries.BinomialHeap.Imp.Heap.fold {α : Type u_1} {β : Type u_2} (le : ααBool) (s : Heap α) (init : β) (f : βαβ) :
                                                                                              β

                                                                                              O(n log n). Fold over the elements of a heap in increasing order, by repeatedly pulling the minimum element out of the heap.

                                                                                              Equations
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  def Batteries.BinomialHeap.Imp.Heap.toArray {α : Type u_1} (le : ααBool) (s : Heap α) :

                                                                                                  O(n log n). Convert the heap to an array in increasing order.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      @[inline]
                                                                                                      def Batteries.BinomialHeap.Imp.Heap.toList {α : Type u_1} (le : ααBool) (s : Heap α) :
                                                                                                      List α

                                                                                                      O(n log n). Convert the heap to a list in increasing order.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          @[specialize #[]]
                                                                                                          def Batteries.BinomialHeap.Imp.HeapNode.foldTreeM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (nil : β) (join : αββm β) :
                                                                                                          HeapNode αm β

                                                                                                          O(n). Fold a monadic function over the tree structure to accumulate a value.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              @[specialize #[]]
                                                                                                              def Batteries.BinomialHeap.Imp.Heap.foldTreeM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (nil : β) (join : αββm β) :
                                                                                                              Heap αm β

                                                                                                              O(n). Fold a monadic function over the tree structure to accumulate a value.

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  @[inline]
                                                                                                                  def Batteries.BinomialHeap.Imp.Heap.foldTree {β : Type u_1} {α : Type u_2} (nil : β) (join : αβββ) (s : Heap α) :
                                                                                                                  β

                                                                                                                  O(n). Fold a function over the tree structure to accumulate a value.

                                                                                                                  Equations
                                                                                                                    Instances For

                                                                                                                      O(n). Convert the heap to a list in arbitrary order.

                                                                                                                      Equations
                                                                                                                        Instances For

                                                                                                                          O(n). Convert the heap to an array in arbitrary order.

                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              def Batteries.BinomialHeap.Imp.HeapNode.WF {α : Type u_1} (le : ααBool) (a : α) :
                                                                                                                              HeapNode αNatProp

                                                                                                                              The well formedness predicate for a heap node. It asserts that:

                                                                                                                              • If a is added at the top to make the forest into a tree, the resulting tree is a le-min-heap (if le is well-behaved)
                                                                                                                              • When interpreting child and sibling as left and right children of a binary tree, it is a perfect binary tree with depth r
                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  def Batteries.BinomialHeap.Imp.Heap.WF {α : Type u_1} (le : ααBool) (n : Nat) :
                                                                                                                                  Heap αProp

                                                                                                                                  The well formedness predicate for a binomial heap. It asserts that:

                                                                                                                                  • It consists of a list of well formed trees with the specified ranks
                                                                                                                                  • The ranks are in strictly increasing order, and all are at least n
                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.Heap.WF.nil {α✝ : Type u_1} {le : α✝α✝Bool} {n : Nat} :
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.Heap.WF.singleton {α✝ : Type u_1} {a : α✝} {le : α✝α✝Bool} :
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.Heap.WF.of_rankGT {α✝ : Type u_1} {le : α✝α✝Bool} {n' : Nat} {s : Heap α✝} {n : Nat} (hlt : s.rankGT n) (h : WF le n' s) :
                                                                                                                                      WF le (n + 1) s
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.Heap.WF.of_le {n n' : Nat} {α✝ : Type u_1} {le : α✝α✝Bool} {s : Heap α✝} (hle : n n') (h : WF le n' s) :
                                                                                                                                      WF le n s
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.Heap.rankGT.of_le {α✝ : Type u_1} {s : Heap α✝} {n n' : Nat} (h : s.rankGT n) (h' : n' n) :
                                                                                                                                      s.rankGT n'
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.Heap.WF.rankGT {α✝ : Type u_1} {lt : α✝α✝Bool} {n : Nat} {s : Heap α✝} (h : WF lt (n + 1) s) :
                                                                                                                                      s.rankGT n
                                                                                                                                      @[irreducible]
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.Heap.WF.merge' {α✝ : Type u_1} {le : α✝α✝Bool} {s₁ s₂ : Heap α✝} {n : Nat} (h₁ : WF le n s₁) (h₂ : WF le n s₂) :
                                                                                                                                      WF le n (Heap.merge le s₁ s₂) ((s₁.rankGT n s₂.rankGT n) → (Heap.merge le s₁ s₂).rankGT n)
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.Heap.WF.merge {α✝ : Type u_1} {le : α✝α✝Bool} {s₁ s₂ : Heap α✝} {n : Nat} (h₁ : WF le n s₁) (h₂ : WF le n s₂) :
                                                                                                                                      WF le n (Heap.merge le s₁ s₂)
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.HeapNode.WF.rank_eq {α : Type u_1} {le : ααBool} {a : α} {n : Nat} {s : HeapNode α} :
                                                                                                                                      WF le a s ns.rank = n
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.HeapNode.WF.toHeap {α : Type u_1} {le : ααBool} {a : α} {n : Nat} {s : HeapNode α} (h : WF le a s n) :
                                                                                                                                      theorem Batteries.BinomialHeap.Imp.HeapNode.WF.toHeap.go {α : Type u_1} {le : ααBool} {a : α} {res : Heap α} {n : Nat} {s : HeapNode α} :
                                                                                                                                      WF le a s nHeap.WF le s.rank resHeap.WF le 0 (HeapNode.toHeap.go s s.rank res)
                                                                                                                                      structure Batteries.BinomialHeap.Imp.FindMin.WF {α : Type u_1} (le : ααBool) (res : FindMin α) :

                                                                                                                                      The well formedness predicate for a FindMin value. This is not actually a predicate, as it contains an additional data value rank corresponding to the rank of the returned node, which is omitted from findMin.

                                                                                                                                      Instances For
                                                                                                                                        def Batteries.BinomialHeap.Imp.Heap.WF.findMin {α : Type u_1} {le : ααBool} {n : Nat} {k : Heap αHeap α} {res : FindMin α} {s : Heap α} (h : WF le n s) (hr : FindMin.WF le res) (hk : ∀ {s : Heap α}, WF le n sWF le 0 (k s)) :
                                                                                                                                        FindMin.WF le (Heap.findMin le k s res)

                                                                                                                                        The conditions under which findMin is well-formed.

                                                                                                                                        Equations
                                                                                                                                          Instances For
                                                                                                                                            theorem Batteries.BinomialHeap.Imp.Heap.WF.deleteMin {α : Type u_1} {le : ααBool} {n : Nat} {a : α} {s' s : Heap α} (h : WF le n s) (eq : Heap.deleteMin le s = some (a, s')) :
                                                                                                                                            WF le 0 s'
                                                                                                                                            theorem Batteries.BinomialHeap.Imp.Heap.WF.tail? {α : Type u_1} {s : Heap α} {le : ααBool} {n : Nat} {tl : Heap α} (hwf : WF le n s) :
                                                                                                                                            Heap.tail? le s = some tlWF le 0 tl
                                                                                                                                            theorem Batteries.BinomialHeap.Imp.Heap.WF.tail {α : Type u_1} {s : Heap α} {le : ααBool} {n : Nat} (hwf : WF le n s) :
                                                                                                                                            WF le 0 (Heap.tail le s)
                                                                                                                                            def Batteries.BinomialHeap (α : Type u) (le : ααBool) :

                                                                                                                                            A binomial heap is a data structure which supports the following primary operations:

                                                                                                                                            The first two operations are known as a "priority queue", so this could be called a "mergeable priority queue". The standard choice for a priority queue is a binary heap, which supports insert and deleteMin in O(log n), but merge is O(n). With a BinomialHeap, all three operations are O(log n).

                                                                                                                                            Equations
                                                                                                                                              Instances For
                                                                                                                                                @[inline]
                                                                                                                                                def Batteries.mkBinomialHeap (α : Type u) (le : ααBool) :

                                                                                                                                                O(1). Make a new empty binomial heap.

                                                                                                                                                Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[inline]
                                                                                                                                                    def Batteries.BinomialHeap.empty {α : Type u} {le : ααBool} :

                                                                                                                                                    O(1). Make a new empty binomial heap.

                                                                                                                                                    Equations
                                                                                                                                                      Instances For
                                                                                                                                                        instance Batteries.BinomialHeap.instEmptyCollection {α : Type u} {le : ααBool} :
                                                                                                                                                        Equations
                                                                                                                                                          instance Batteries.BinomialHeap.instInhabited {α : Type u} {le : ααBool} :
                                                                                                                                                          Equations
                                                                                                                                                            @[inline]
                                                                                                                                                            def Batteries.BinomialHeap.isEmpty {α : Type u} {le : ααBool} (b : BinomialHeap α le) :

                                                                                                                                                            O(1). Is the heap empty?

                                                                                                                                                            Equations
                                                                                                                                                              Instances For
                                                                                                                                                                @[inline]
                                                                                                                                                                def Batteries.BinomialHeap.size {α : Type u} {le : ααBool} (b : BinomialHeap α le) :

                                                                                                                                                                O(log n). The number of elements in the heap.

                                                                                                                                                                Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[inline]
                                                                                                                                                                    def Batteries.BinomialHeap.singleton {α : Type u} {le : ααBool} (a : α) :

                                                                                                                                                                    O(1). Make a new heap containing a.

                                                                                                                                                                    Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[inline]
                                                                                                                                                                        def Batteries.BinomialHeap.merge {α : Type u} {le : ααBool} :
                                                                                                                                                                        BinomialHeap α leBinomialHeap α leBinomialHeap α le

                                                                                                                                                                        O(log n). Merge the contents of two heaps.

                                                                                                                                                                        Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[inline]
                                                                                                                                                                            def Batteries.BinomialHeap.insert {α : Type u} {le : ααBool} (a : α) (h : BinomialHeap α le) :

                                                                                                                                                                            O(log n). Add element a to the given heap h.

                                                                                                                                                                            Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                def Batteries.BinomialHeap.ofList {α : Type u} (le : ααBool) (as : List α) :

                                                                                                                                                                                O(n log n). Construct a heap from a list by inserting all the elements.

                                                                                                                                                                                Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    def Batteries.BinomialHeap.ofArray {α : Type u} (le : ααBool) (as : Array α) :

                                                                                                                                                                                    O(n log n). Construct a heap from a list by inserting all the elements.

                                                                                                                                                                                    Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[inline]
                                                                                                                                                                                        def Batteries.BinomialHeap.deleteMin {α : Type u} {le : ααBool} (b : BinomialHeap α le) :

                                                                                                                                                                                        O(log n). Remove and return the minimum element from the heap.

                                                                                                                                                                                        Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            instance Batteries.BinomialHeap.instStream {α : Type u} {le : ααBool} :
                                                                                                                                                                                            Stream (BinomialHeap α le) α
                                                                                                                                                                                            Equations
                                                                                                                                                                                              def Batteries.BinomialHeap.forIn {α : Type u} {le : ααBool} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (b : BinomialHeap α le) (x : β) (f : αβm (ForInStep β)) :
                                                                                                                                                                                              m β

                                                                                                                                                                                              O(n log n). Implementation of for x in (b : BinomialHeap α le) ... notation, which iterates over the elements in the heap in increasing order.

                                                                                                                                                                                              Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  instance Batteries.BinomialHeap.instForIn {α : Type u} {le : ααBool} {m : Type u_1 → Type u_2} :
                                                                                                                                                                                                  ForIn m (BinomialHeap α le) α
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                    def Batteries.BinomialHeap.head? {α : Type u} {le : ααBool} (b : BinomialHeap α le) :

                                                                                                                                                                                                    O(log n). Returns the smallest element in the heap, or none if the heap is empty.

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                        def Batteries.BinomialHeap.head! {α : Type u} {le : ααBool} [Inhabited α] (b : BinomialHeap α le) :
                                                                                                                                                                                                        α

                                                                                                                                                                                                        O(log n). Returns the smallest element in the heap, or panics if the heap is empty.

                                                                                                                                                                                                        Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                            def Batteries.BinomialHeap.headI {α : Type u} {le : ααBool} [Inhabited α] (b : BinomialHeap α le) :
                                                                                                                                                                                                            α

                                                                                                                                                                                                            O(log n). Returns the smallest element in the heap, or default if the heap is empty.

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                def Batteries.BinomialHeap.tail? {α : Type u} {le : ααBool} (b : BinomialHeap α le) :

                                                                                                                                                                                                                O(log n). Removes the smallest element from the heap, or none if the heap is empty.

                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                    def Batteries.BinomialHeap.tail {α : Type u} {le : ααBool} (b : BinomialHeap α le) :

                                                                                                                                                                                                                    O(log n). Removes the smallest element from the heap, if possible.

                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                        def Batteries.BinomialHeap.foldM {α : Type u} {le : ααBool} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (b : BinomialHeap α le) (init : β) (f : βαm β) :
                                                                                                                                                                                                                        m β

                                                                                                                                                                                                                        O(n log n). Monadic fold over the elements of a heap in increasing order, by repeatedly pulling the minimum element out of the heap.

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                            def Batteries.BinomialHeap.fold {α : Type u} {le : ααBool} {β : Type u_1} (b : BinomialHeap α le) (init : β) (f : βαβ) :
                                                                                                                                                                                                                            β

                                                                                                                                                                                                                            O(n log n). Fold over the elements of a heap in increasing order, by repeatedly pulling the minimum element out of the heap.

                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                def Batteries.BinomialHeap.toList {α : Type u} {le : ααBool} (b : BinomialHeap α le) :
                                                                                                                                                                                                                                List α

                                                                                                                                                                                                                                O(n log n). Convert the heap to a list in increasing order.

                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                    def Batteries.BinomialHeap.toArray {α : Type u} {le : ααBool} (b : BinomialHeap α le) :

                                                                                                                                                                                                                                    O(n log n). Convert the heap to an array in increasing order.

                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                        def Batteries.BinomialHeap.toListUnordered {α : Type u} {le : ααBool} (b : BinomialHeap α le) :
                                                                                                                                                                                                                                        List α

                                                                                                                                                                                                                                        O(n). Convert the heap to a list in arbitrary order.

                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                            def Batteries.BinomialHeap.toArrayUnordered {α : Type u} {le : ααBool} (b : BinomialHeap α le) :

                                                                                                                                                                                                                                            O(n). Convert the heap to an array in arbitrary order.

                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                              Instances For