From 745ed4f35baea4b1da38c5d8be6851d6c5c9e728 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Tue, 13 Aug 2024 20:57:10 +0200
Subject: Fix wrong index validity check for Nat indices.

---
 BinaryHeap.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'BinaryHeap.lean')

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
-- 
cgit v1.2.3