From b1821bdf7fb928be27a9919f4969883a2f6670ff Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Tue, 27 Aug 2024 22:59:11 +0200
Subject: Simplify CompleteTree.get, and remove (redundant) CompleteTree.get'

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

(limited to 'BinaryHeap.lean')

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