inductive Batteries.PairingHeapImp.Heap (α : Type u) : Type u

A Heap is the nodes of the pairing heap. Each node have two pointers: child 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} → Batteries.PairingHeapImp.Heap α

  An empty forest, which has depth 0.

• node: {α : Type u} → α → Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α

  A forest consists of a root a, a forest child elements greater than a, and another forest sibling.

instance Batteries.PairingHeapImp.instReprHeap : {α : Type u_1} → [inst : Repr α] → Repr (Batteries.PairingHeapImp.Heap α)

Equations

• Batteries.PairingHeapImp.instReprHeap = { reprPrec := Batteries.PairingHeapImp.reprHeap✝ }

def Batteries.PairingHeapImp.Heap.size {α : Type u_1} : Batteries.PairingHeapImp.Heap α → Nat

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

Equations

• Batteries.PairingHeapImp.Heap.nil.size = 0
• (Batteries.PairingHeapImp.Heap.node a a_1 a_2).size = a_1.size + 1 + a_2.size

def Batteries.PairingHeapImp.Heap.singleton {α : Type u_1} (a : α) : Batteries.PairingHeapImp.Heap α

A node containing a single element a.

Equations

• Batteries.PairingHeapImp.Heap.singleton a = Batteries.PairingHeapImp.Heap.node a Batteries.PairingHeapImp.Heap.nil Batteries.PairingHeapImp.Heap.nil

def Batteries.PairingHeapImp.Heap.isEmpty {α : Type u_1} : Batteries.PairingHeapImp.Heap α → Bool

O(1). Is the heap empty?

Equations

• Batteries.PairingHeapImp.Heap.nil.isEmpty = true
• x.isEmpty = false

@[specialize #[]]

def Batteries.PairingHeapImp.Heap.merge {α : Type u_1} (le : α → α → Bool) : Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α

O(1). Merge two heaps. Ignore siblings.

Equations

• One or more equations did not get rendered due to their size.
• Batteries.PairingHeapImp.Heap.merge le Batteries.PairingHeapImp.Heap.nil Batteries.PairingHeapImp.Heap.nil = Batteries.PairingHeapImp.Heap.nil

@[specialize #[]]

def Batteries.PairingHeapImp.Heap.combine {α : Type u_1} (le : α → α → Bool) : Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α

Auxiliary for Heap.deleteMin: merge the forest in pairs.

Equations

• One or more equations did not get rendered due to their size.
• Batteries.PairingHeapImp.Heap.combine le x = x

@[inline]

def Batteries.PairingHeapImp.Heap.headD {α : Type u_1} (a : α) : Batteries.PairingHeapImp.Heap α → α

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

Equations

• Batteries.PairingHeapImp.Heap.headD a Batteries.PairingHeapImp.Heap.nil = a
• Batteries.PairingHeapImp.Heap.headD a (Batteries.PairingHeapImp.Heap.node a_1 a_2 a_3) = a_1

@[inline]

def Batteries.PairingHeapImp.Heap.head? {α : Type u_1} : Batteries.PairingHeapImp.Heap α → Option α

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

Equations

• Batteries.PairingHeapImp.Heap.nil.head? = none
• (Batteries.PairingHeapImp.Heap.node a a_1 a_2).head? = some a

@[inline]

def Batteries.PairingHeapImp.Heap.deleteMin {α : Type u_1} (le : α → α → Bool) : Batteries.PairingHeapImp.Heap α → Option (α × Batteries.PairingHeapImp.Heap α)

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

Equations

• Batteries.PairingHeapImp.Heap.deleteMin le Batteries.PairingHeapImp.Heap.nil = none
• Batteries.PairingHeapImp.Heap.deleteMin le (Batteries.PairingHeapImp.Heap.node a a_1 a_2) = some (a, Batteries.PairingHeapImp.Heap.combine le a_1)

@[inline]

def Batteries.PairingHeapImp.Heap.tail? {α : Type u_1} (le : α → α → Bool) (h : Batteries.PairingHeapImp.Heap α) : Option (Batteries.PairingHeapImp.Heap α)

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

Equations

• Batteries.PairingHeapImp.Heap.tail? le h = Option.map (fun (x : α × Batteries.PairingHeapImp.Heap α) => x.snd) (Batteries.PairingHeapImp.Heap.deleteMin le h)

@[inline]

def Batteries.PairingHeapImp.Heap.tail {α : Type u_1} (le : α → α → Bool) (h : Batteries.PairingHeapImp.Heap α) : Batteries.PairingHeapImp.Heap α

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

Equations

• Batteries.PairingHeapImp.Heap.tail le h = (Batteries.PairingHeapImp.Heap.tail? le h).getD Batteries.PairingHeapImp.Heap.nil

inductive Batteries.PairingHeapImp.Heap.NoSibling {α : Type u_1} : Batteries.PairingHeapImp.Heap α → Prop

A predicate says there is no more than one tree.

• nil: ∀ {α : Type u_1}, Batteries.PairingHeapImp.Heap.nil.NoSibling

  An empty heap is no more than one tree.

• node: ∀ {α : Type u_1} (a : α) (c : Batteries.PairingHeapImp.Heap α), (Batteries.PairingHeapImp.Heap.node a c Batteries.PairingHeapImp.Heap.nil).NoSibling

  Or there is exactly one tree.

instance Batteries.PairingHeapImp.instDecidableNoSibling : {α : Type u_1} → {s : Batteries.PairingHeapImp.Heap α} → Decidable s.NoSibling

Equations

• Batteries.PairingHeapImp.instDecidableNoSibling = isTrue ⋯
• Batteries.PairingHeapImp.instDecidableNoSibling = isTrue ⋯
• Batteries.PairingHeapImp.instDecidableNoSibling = isFalse ⋯

theorem Batteries.PairingHeapImp.Heap.noSibling_merge {α : Type u_1} (le : α → α → Bool) (s₁ : Batteries.PairingHeapImp.Heap α) (s₂ : Batteries.PairingHeapImp.Heap α) : (Batteries.PairingHeapImp.Heap.merge le s₁ s₂).NoSibling

theorem Batteries.PairingHeapImp.Heap.noSibling_combine {α : Type u_1} (le : α → α → Bool) (s : Batteries.PairingHeapImp.Heap α) : (Batteries.PairingHeapImp.Heap.combine le s).NoSibling

theorem Batteries.PairingHeapImp.Heap.noSibling_deleteMin {α : Type u_1} {le : α → α → Bool} {a : α} {s' : Batteries.PairingHeapImp.Heap α} {s : Batteries.PairingHeapImp.Heap α} (eq : Batteries.PairingHeapImp.Heap.deleteMin le s = some (a, s')) : s'.NoSibling

theorem Batteries.PairingHeapImp.Heap.noSibling_tail? {α : Type u_1} {le : α → α → Bool} {s' : Batteries.PairingHeapImp.Heap α} {s : Batteries.PairingHeapImp.Heap α} : Batteries.PairingHeapImp.Heap.tail? le s = some s' → s'.NoSibling

theorem Batteries.PairingHeapImp.Heap.noSibling_tail {α : Type u_1} (le : α → α → Bool) (s : Batteries.PairingHeapImp.Heap α) : (Batteries.PairingHeapImp.Heap.tail le s).NoSibling

theorem Batteries.PairingHeapImp.Heap.size_merge_node {α : Type u_1} (le : α → α → Bool) (a₁ : α) (c₁ : Batteries.PairingHeapImp.Heap α) (s₁ : Batteries.PairingHeapImp.Heap α) (a₂ : α) (c₂ : Batteries.PairingHeapImp.Heap α) (s₂ : Batteries.PairingHeapImp.Heap α) : (Batteries.PairingHeapImp.Heap.merge le (Batteries.PairingHeapImp.Heap.node a₁ c₁ s₁) (Batteries.PairingHeapImp.Heap.node a₂ c₂ s₂)).size = c₁.size + c₂.size + 2

theorem Batteries.PairingHeapImp.Heap.size_merge {α : Type u_1} (le : α → α → Bool) {s₁ : Batteries.PairingHeapImp.Heap α} {s₂ : Batteries.PairingHeapImp.Heap α} (h₁ : s₁.NoSibling) (h₂ : s₂.NoSibling) : (Batteries.PairingHeapImp.Heap.merge le s₁ s₂).size = s₁.size + s₂.size

@[irreducible]

theorem Batteries.PairingHeapImp.Heap.size_combine {α : Type u_1} (le : α → α → Bool) (s : Batteries.PairingHeapImp.Heap α) : (Batteries.PairingHeapImp.Heap.combine le s).size = s.size

theorem Batteries.PairingHeapImp.Heap.size_deleteMin {α : Type u_1} {le : α → α → Bool} {a : α} {s' : Batteries.PairingHeapImp.Heap α} {s : Batteries.PairingHeapImp.Heap α} (h : s.NoSibling) (eq : Batteries.PairingHeapImp.Heap.deleteMin le s = some (a, s')) : s.size = s'.size + 1

theorem Batteries.PairingHeapImp.Heap.size_tail? {α : Type u_1} {le : α → α → Bool} {s' : Batteries.PairingHeapImp.Heap α} {s : Batteries.PairingHeapImp.Heap α} (h : s.NoSibling) : Batteries.PairingHeapImp.Heap.tail? le s = some s' → s.size = s'.size + 1

theorem Batteries.PairingHeapImp.Heap.size_tail {α : Type u_1} (le : α → α → Bool) {s : Batteries.PairingHeapImp.Heap α} (h : s.NoSibling) : (Batteries.PairingHeapImp.Heap.tail le s).size = s.size - 1

theorem Batteries.PairingHeapImp.Heap.size_deleteMin_lt {α : Type u_1} {le : α → α → Bool} {a : α} {s' : Batteries.PairingHeapImp.Heap α} {s : Batteries.PairingHeapImp.Heap α} (eq : Batteries.PairingHeapImp.Heap.deleteMin le s = some (a, s')) : s'.size < s.size

theorem Batteries.PairingHeapImp.Heap.size_tail?_lt {α : Type u_1} {le : α → α → Bool} {s' : Batteries.PairingHeapImp.Heap α} {s : Batteries.PairingHeapImp.Heap α} : Batteries.PairingHeapImp.Heap.tail? le s = some s' → s'.size < s.size

@[irreducible, specialize #[]]

def Batteries.PairingHeapImp.Heap.foldM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (le : α → α → Bool) (s : Batteries.PairingHeapImp.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

• One or more equations did not get rendered due to their size.

@[inline]

def Batteries.PairingHeapImp.Heap.fold {α : Type u_1} {β : Type u_2} (le : α → α → Bool) (s : Batteries.PairingHeapImp.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

• Batteries.PairingHeapImp.Heap.fold le s init f = (Batteries.PairingHeapImp.Heap.foldM le s init f).run

@[inline]

def Batteries.PairingHeapImp.Heap.toArray {α : Type u_1} (le : α → α → Bool) (s : Batteries.PairingHeapImp.Heap α) : Array α

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

Equations

• Batteries.PairingHeapImp.Heap.toArray le s = Batteries.PairingHeapImp.Heap.fold le s #[] Array.push

@[inline]

def Batteries.PairingHeapImp.Heap.toList {α : Type u_1} (le : α → α → Bool) (s : Batteries.PairingHeapImp.Heap α) : List α

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

Equations

• Batteries.PairingHeapImp.Heap.toList le s = (Batteries.PairingHeapImp.Heap.toArray le s).toList

@[specialize #[]]

def Batteries.PairingHeapImp.Heap.foldTreeM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (nil : β) (join : α → β → β → m β) : Batteries.PairingHeapImp.Heap α → m β

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

Equations

• One or more equations did not get rendered due to their size.
• Batteries.PairingHeapImp.Heap.foldTreeM nil join Batteries.PairingHeapImp.Heap.nil = pure nil

@[inline]

def Batteries.PairingHeapImp.Heap.foldTree {β : Type u_1} {α : Type u_2} (nil : β) (join : α → β → β → β) (s : Batteries.PairingHeapImp.Heap α) : β

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

Equations

• Batteries.PairingHeapImp.Heap.foldTree nil join s = (Batteries.PairingHeapImp.Heap.foldTreeM nil join s).run

def Batteries.PairingHeapImp.Heap.toListUnordered {α : Type u_1} (s : Batteries.PairingHeapImp.Heap α) : List α

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

Equations

• s.toListUnordered = Batteries.PairingHeapImp.Heap.foldTree id (fun (a : α) (c s : List α → List α) (l : List α) => a :: c (s l)) s []

def Batteries.PairingHeapImp.Heap.toArrayUnordered {α : Type u_1} (s : Batteries.PairingHeapImp.Heap α) : Array α

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

Equations

• s.toArrayUnordered = Batteries.PairingHeapImp.Heap.foldTree id (fun (a : α) (c s : Array α → Array α) (r : Array α) => s (c (r.push a))) s #[]

def Batteries.PairingHeapImp.Heap.NodeWF {α : Type u_1} (le : α → α → Bool) (a : α) : Batteries.PairingHeapImp.Heap α → Prop

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)

Equations

• One or more equations did not get rendered due to their size.
• Batteries.PairingHeapImp.Heap.NodeWF le a Batteries.PairingHeapImp.Heap.nil = True

inductive Batteries.PairingHeapImp.Heap.WF {α : Type u_1} (le : α → α → Bool) : Batteries.PairingHeapImp.Heap α → Prop

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

• There is no more than one tree.
• It is a le-min-heap (if le is well-behaved)

• nil: ∀ {α : Type u_1} {le : α → α → Bool}, Batteries.PairingHeapImp.Heap.WF le Batteries.PairingHeapImp.Heap.nil

  It is an empty heap.

• node: ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {c : Batteries.PairingHeapImp.Heap α}, Batteries.PairingHeapImp.Heap.NodeWF le a c → Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.node a c Batteries.PairingHeapImp.Heap.nil)

  There is exactly one tree and it is a le-min-heap.

theorem Batteries.PairingHeapImp.Heap.WF.singleton : ∀ {α : Type u_1} {a : α} {le : α → α → Bool}, Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.singleton a)

theorem Batteries.PairingHeapImp.Heap.WF.merge_node : ∀ {α : Type u_1} {le : α → α → Bool} {a₁ : α} {c₁ : Batteries.PairingHeapImp.Heap α} {a₂ : α} {c₂ s₁ s₂ : Batteries.PairingHeapImp.Heap α}, Batteries.PairingHeapImp.Heap.NodeWF le a₁ c₁ → Batteries.PairingHeapImp.Heap.NodeWF le a₂ c₂ → Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.merge le (Batteries.PairingHeapImp.Heap.node a₁ c₁ s₁) (Batteries.PairingHeapImp.Heap.node a₂ c₂ s₂))

theorem Batteries.PairingHeapImp.Heap.WF.merge : ∀ {α : Type u_1} {le : α → α → Bool} {s₁ s₂ : Batteries.PairingHeapImp.Heap α}, Batteries.PairingHeapImp.Heap.WF le s₁ → Batteries.PairingHeapImp.Heap.WF le s₂ → Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.merge le s₁ s₂)

theorem Batteries.PairingHeapImp.Heap.WF.combine : ∀ {α : Type u_1} {le : α → α → Bool} {s : Batteries.PairingHeapImp.Heap α} {a : α}, Batteries.PairingHeapImp.Heap.NodeWF le a s → Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.combine le s)

theorem Batteries.PairingHeapImp.Heap.WF.deleteMin {α : Type u_1} {le : α → α → Bool} {a : α} {s' : Batteries.PairingHeapImp.Heap α} {s : Batteries.PairingHeapImp.Heap α} (h : Batteries.PairingHeapImp.Heap.WF le s) (eq : Batteries.PairingHeapImp.Heap.deleteMin le s = some (a, s')) : Batteries.PairingHeapImp.Heap.WF le s'

theorem Batteries.PairingHeapImp.Heap.WF.tail? {α : Type u_1} {s : Batteries.PairingHeapImp.Heap α} {le : α → α → Bool} {tl : Batteries.PairingHeapImp.Heap α} (hwf : Batteries.PairingHeapImp.Heap.WF le s) : Batteries.PairingHeapImp.Heap.tail? le s = some tl → Batteries.PairingHeapImp.Heap.WF le tl

theorem Batteries.PairingHeapImp.Heap.WF.tail {α : Type u_1} {s : Batteries.PairingHeapImp.Heap α} {le : α → α → Bool} (hwf : Batteries.PairingHeapImp.Heap.WF le s) : Batteries.PairingHeapImp.Heap.WF le (Batteries.PairingHeapImp.Heap.tail le s)

theorem Batteries.PairingHeapImp.Heap.deleteMin_fst {α : Type u_1} {s : Batteries.PairingHeapImp.Heap α} {le : α → α → Bool} : Option.map (fun (x : α × Batteries.PairingHeapImp.Heap α) => x.fst) (Batteries.PairingHeapImp.Heap.deleteMin le s) = s.head?

def Batteries.PairingHeap (α : Type u) (le : α → α → Bool) : Type (max 0 u)

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

• insert : α → PairingHeap α → PairingHeap α: add an element to the heap
• deleteMin : PairingHeap α → Option (α × PairingHeap α): remove the minimum element from the heap
• merge : PairingHeap α → PairingHeap α → PairingHeap α: combine two heaps

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 PairingHeap, insert and merge are O(1), deleteMin is amortized O(log n).

Note that deleteMin may be O(n) in a single operation. So if you need an efficient persistent priority queue, you should use other data structures with better worst-case time.

Equations

• Batteries.PairingHeap α le = { h : Batteries.PairingHeapImp.Heap α // Batteries.PairingHeapImp.Heap.WF le h }

@[inline]

def Batteries.mkPairingHeap (α : Type u) (le : α → α → Bool) : Batteries.PairingHeap α le

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

Equations

• Batteries.mkPairingHeap α le = ⟨Batteries.PairingHeapImp.Heap.nil, ⋯⟩

@[inline]

def Batteries.PairingHeap.empty {α : Type u} {le : α → α → Bool} : Batteries.PairingHeap α le

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

Equations

• Batteries.PairingHeap.empty = Batteries.mkPairingHeap α le

instance Batteries.PairingHeap.instInhabited {α : Type u} {le : α → α → Bool} : Inhabited (Batteries.PairingHeap α le)

Equations

• Batteries.PairingHeap.instInhabited = { default := Batteries.PairingHeap.empty }

@[inline]

def Batteries.PairingHeap.isEmpty {α : Type u} {le : α → α → Bool} (b : Batteries.PairingHeap α le) : Bool

O(1). Is the heap empty?

Equations

• b.isEmpty = b.val.isEmpty

@[inline]

def Batteries.PairingHeap.size {α : Type u} {le : α → α → Bool} (b : Batteries.PairingHeap α le) : Nat

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

Equations

• b.size = b.val.size

@[inline]

def Batteries.PairingHeap.singleton {α : Type u} {le : α → α → Bool} (a : α) : Batteries.PairingHeap α le

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

Equations

• Batteries.PairingHeap.singleton a = ⟨Batteries.PairingHeapImp.Heap.singleton a, ⋯⟩

@[inline]

def Batteries.PairingHeap.merge {α : Type u} {le : α → α → Bool} : Batteries.PairingHeap α le → Batteries.PairingHeap α le → Batteries.PairingHeap α le

O(1). Merge the contents of two heaps.

Equations

• Batteries.PairingHeap.merge ⟨b₁, h₁⟩ ⟨b₂, h₂⟩ = ⟨Batteries.PairingHeapImp.Heap.merge le b₁ b₂, ⋯⟩

@[inline]

def Batteries.PairingHeap.insert {α : Type u} {le : α → α → Bool} (a : α) (h : Batteries.PairingHeap α le) : Batteries.PairingHeap α le

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

Equations

• Batteries.PairingHeap.insert a h = (Batteries.PairingHeap.singleton a).merge h

def Batteries.PairingHeap.ofList {α : Type u} (le : α → α → Bool) (as : List α) : Batteries.PairingHeap α le

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

Equations

• Batteries.PairingHeap.ofList le as = List.foldl (flip Batteries.PairingHeap.insert) Batteries.PairingHeap.empty as

def Batteries.PairingHeap.ofArray {α : Type u} (le : α → α → Bool) (as : Array α) : Batteries.PairingHeap α le

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

Equations

• Batteries.PairingHeap.ofArray le as = Array.foldl (flip Batteries.PairingHeap.insert) Batteries.PairingHeap.empty as

@[inline]

def Batteries.PairingHeap.deleteMin {α : Type u} {le : α → α → Bool} (b : Batteries.PairingHeap α le) : Option (α × Batteries.PairingHeap α le)

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

Equations

• b.deleteMin = match eq : Batteries.PairingHeapImp.Heap.deleteMin le b.val with | none => none | some (a, tl) => some (a, ⟨tl, ⋯⟩)

@[inline]

def Batteries.PairingHeap.head? {α : Type u} {le : α → α → Bool} (b : Batteries.PairingHeap α le) : Option α

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

Equations

• b.head? = b.val.head?

@[inline]

def Batteries.PairingHeap.head! {α : Type u} {le : α → α → Bool} [Inhabited α] (b : Batteries.PairingHeap α le) : α

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

Equations

• b.head! = b.head?.get!

@[inline]

def Batteries.PairingHeap.headI {α : Type u} {le : α → α → Bool} [Inhabited α] (b : Batteries.PairingHeap α le) : α

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

Equations

• b.headI = b.head?.getD default

@[inline]

def Batteries.PairingHeap.tail? {α : Type u} {le : α → α → Bool} (b : Batteries.PairingHeap α le) : Option (Batteries.PairingHeap α le)

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

Equations

• b.tail? = match eq : Batteries.PairingHeapImp.Heap.tail? le b.val with | none => none | some tl => some ⟨tl, ⋯⟩

@[inline]

def Batteries.PairingHeap.tail {α : Type u} {le : α → α → Bool} (b : Batteries.PairingHeap α le) : Batteries.PairingHeap α le

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

Equations

• b.tail = ⟨Batteries.PairingHeapImp.Heap.tail le b.val, ⋯⟩

@[inline]

def Batteries.PairingHeap.toList {α : Type u} {le : α → α → Bool} (b : Batteries.PairingHeap α le) : List α

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

Equations

• b.toList = Batteries.PairingHeapImp.Heap.toList le b.val

@[inline]

def Batteries.PairingHeap.toArray {α : Type u} {le : α → α → Bool} (b : Batteries.PairingHeap α le) : Array α

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

Equations

• b.toArray = Batteries.PairingHeapImp.Heap.toArray le b.val

@[inline]

def Batteries.PairingHeap.toListUnordered {α : Type u} {le : α → α → Bool} (b : Batteries.PairingHeap α le) : List α

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

Equations

• b.toListUnordered = b.val.toListUnordered

@[inline]

def Batteries.PairingHeap.toArrayUnordered {α : Type u} {le : α → α → Bool} (b : Batteries.PairingHeap α le) : Array α

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

Equations

• b.toArrayUnordered = b.val.toArrayUnordered