diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-27 22:59:11 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-27 22:59:11 +0200 |
| commit | b1821bdf7fb928be27a9919f4969883a2f6670ff (patch) | |
| tree | 0597222a585b1e34c733390068ed9f35ad55bec1 /BinaryHeap.lean | |
| parent | 3bdc50ac878c1b6d066a342d2b4909b1b4e841d9 (diff) | |
Simplify CompleteTree.get, and remove (redundant) CompleteTree.get'
Diffstat (limited to 'BinaryHeap.lean')
| -rw-r--r-- | BinaryHeap.lean | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/BinaryHeap.lean b/BinaryHeap.lean index 61ebd42..4c7326f 100644 --- a/BinaryHeap.lean +++ b/BinaryHeap.lean @@ -53,12 +53,10 @@ def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le tree.indexOf pred instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index < n) where - getElem := λ heap index h₁ ↦ match n, heap, index with - | (_+1), {tree, ..}, index => tree.get' ⟨index, h₁⟩ + getElem := λ heap index h₁ ↦ heap.tree.get ⟨index, h₁⟩ instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ True) where - getElem := λ heap index _ ↦ match n, heap, index with - | (_+1), {tree, ..}, index => tree.get' index + getElem := λ heap index _ ↦ heap.tree.get index /--Helper for the common case of using natural numbers for sorting.-/ theorem nat_ble_to_heap_le_total : total_le Nat.ble := |