diff options
| -rw-r--r-- | BinaryHeap/Aux.lean | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/BinaryHeap/Aux.lean b/BinaryHeap/Aux.lean index 0aa052d..1b23bbf 100644 --- a/BinaryHeap/Aux.lean +++ b/BinaryHeap/Aux.lean @@ -27,7 +27,7 @@ def ofList {α : Type u} {le : α → α → Bool} (h₁ : TotalAndTransitiveLe | a :: as => (Nat.add_comm_right n as.length 1).subst rfl ▸ worker as (heap.push a) Nat.zero_add l.length ▸ worker l $ BinaryHeap.new h₁ -/- Converts the tree to a sorted list. -/ +/-- Converts the tree to a sorted list. -/ def toList (heap : BinaryHeap α le n) : List α := let rec worker : (l : List α) → {n : Nat} → (BinaryHeap α le n) → List α := λ(l : List α) {n : Nat} (heap : BinaryHeap α le n) ↦ match n with @@ -37,6 +37,14 @@ def toList (heap : BinaryHeap α le n) : List α := worker (h :: l) hs worker [] heap +/-- Adds all elements in a list -/ +def pushList {α : Type u} {n : Nat} {le : α → α → Bool} (heap : BinaryHeap α le n) (l : List α) : BinaryHeap α le (n+l.length) := + match l with + | [] => heap + | a :: as => + have : n + 1 + as.length = n + (a :: as).length := by simp_arith[List.length_cons a as] + this▸pushList (heap.push a) as + private def ofForInAux [ForIn Id ρ α] {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (c : ρ) : (h : Nat) ×' BinaryHeap α le h := Id.run do let mut r : (h : Nat) ×' BinaryHeap α le h := ⟨0, BinaryHeap.new h₁⟩ for e in c do |