diff options
| author | Andreas Grois <andi@grois.info> | 2024-07-24 23:44:16 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-07-24 23:44:16 +0200 |
| commit | c2111e57923233736b0e2f4cbf2dc8c3da4e91f7 (patch) | |
| tree | 355a8be25085720deb982c162ec0ef10ef7b0e3e /BinaryHeap.lean | |
| parent | 76e6405c9f810bf9830756bb20ad9e4be3214b89 (diff) | |
Start contains_iff_index_exists implementation. Unfinished.
Diffstat (limited to 'BinaryHeap.lean')
| -rw-r--r-- | BinaryHeap.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/BinaryHeap.lean b/BinaryHeap.lean index 9d1da1b..779c3ed 100644 --- a/BinaryHeap.lean +++ b/BinaryHeap.lean @@ -54,11 +54,11 @@ def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index > 0 ∧ index < n) where getElem := λ heap index h₁ ↦ match n, heap, index with - | (_+1), {tree, ..}, index => tree.get ⟨index, h₁.right⟩ + | (_+1), {tree, ..}, index => tree.get' ⟨index, h₁.right⟩ instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ n > 0) where getElem := λ heap index _ ↦ match n, heap, index with - | (_+1), {tree, ..}, index => tree.get index + | (_+1), {tree, ..}, index => 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 := by |