diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-13 20:57:10 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-13 20:57:10 +0200 |
| commit | 745ed4f35baea4b1da38c5d8be6851d6c5c9e728 (patch) | |
| tree | f78b74329b3c7e4890fc943f6288feb03febe39d /BinaryHeap.lean | |
| parent | 8bbaa53546849c018d7546772080951c45ad0c34 (diff) | |
Fix wrong index validity check for Nat indices.
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 779c3ed..4a5bd26 100644 --- a/BinaryHeap.lean +++ b/BinaryHeap.lean @@ -52,9 +52,9 @@ def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le | {tree, valid := _, wellDefinedLe := _}, pred => tree.indexOf pred -instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index > 0 ∧ index < n) where +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₁.right⟩ + | (_+1), {tree, ..}, index => tree.get' ⟨index, h₁⟩ instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ n > 0) where getElem := λ heap index _ ↦ match n, heap, index with |