def Batteries.BinaryHeap.WF.Children {α : Type u_1} {sz : Nat} [Ord α] (a : Vector α sz) (i : Fin sz) : Prop

The primary local correctness property for the heap. A node should be >= both its children (if it has them).

Equations

• Batteries.BinaryHeap.WF.Children a i = ((∀ (x : 2 * ↑i + 1 < sz), (compare a[i] a[2 * ↑i + 1]).isGE = true) ∧ ∀ (x : 2 * ↑i + 1 + 1 < sz), (compare a[i] a[2 * ↑i + 1 + 1]).isGE = true)

def Batteries.BinaryHeap.WF.TopDown {α : Type u_1} {sz : Nat} [Ord α] (v : Vector α sz) : Prop

The vector underlying a BinaryHeap is well-formed iff every node is ≥ any children it has

Equations

• Batteries.BinaryHeap.WF.TopDown v = ∀ (i : Fin sz), Batteries.BinaryHeap.WF.Children v i

def Batteries.BinaryHeap.WF {α : Type u_1} [Ord α] (heap : BinaryHeap α) : Prop

The well-formedness property of a binary heap

Equations

• heap.WF = Batteries.BinaryHeap.WF.TopDown heap.vector