From 3bdc50ac878c1b6d066a342d2b4909b1b4e841d9 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Mon, 26 Aug 2024 19:07:36 +0200
Subject: Minor

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

(limited to 'BinaryHeap.lean')

diff --git a/BinaryHeap.lean b/BinaryHeap.lean
index e3c39af..61ebd42 100644
--- a/BinaryHeap.lean
+++ b/BinaryHeap.lean
@@ -12,7 +12,7 @@ deriving Repr
 namespace BinaryHeap
 
 /-- Creates an empty heap. O(1) -/
-def new (α : Type u) {le : α → α → Bool} (h₁ : BinaryHeap.transitive_le le) (h₂ : BinaryHeap.total_le le) : BinaryHeap α le 0 :=
+def new (α : Type u) {le : α → α → Bool} (h₁ : transitive_le le) (h₂ : total_le le) : BinaryHeap α le 0 :=
   {
     tree := CompleteTree.empty,
     valid := CompleteTree.emptyIsHeap le
@@ -56,7 +56,7 @@ instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index < n) wher
   getElem := λ heap index h₁ ↦ match n, heap, index with
   | (_+1), {tree, ..}, index => tree.get' ⟨index, h₁⟩
 
-instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ n > 0) where
+instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ True) where
   getElem := λ heap index _ ↦ match n, heap, index with
   | (_+1), {tree, ..}, index => tree.get' index
 
-- 
cgit v1.2.3

