From a9ff650577b0b9c35066875d2dce7b4a72e0cb55 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Mon, 26 Aug 2024 00:18:26 +0200
Subject: Remove useless proof parameter on CompleteTree.get

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

(limited to 'BinaryHeap.lean')

diff --git a/BinaryHeap.lean b/BinaryHeap.lean
index 774a3c3..e3c39af 100644
--- a/BinaryHeap.lean
+++ b/BinaryHeap.lean
@@ -41,14 +41,14 @@ def removeAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α
   ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
 
 /-- Updates the element at the given (depth-first) index and returns its previous value. O(log(n)) -/
-def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (Fin (n+1)) → α → (BinaryHeap α le (n+1) × α)
+def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le n) → (Fin n) → α → (BinaryHeap α le n × α)
 | {tree, valid, wellDefinedLe}, index, value =>
-  let result := tree.heapUpdateAt le index value $ Nat.succ_pos n
-  let resultValid := CompleteTree.heapUpdateAtIsHeap le index value tree _ valid wellDefinedLe.left wellDefinedLe.right
+  let result := tree.heapUpdateAt le index value
+  let resultValid := CompleteTree.heapUpdateAtIsHeap le index value tree valid wellDefinedLe.left wellDefinedLe.right
   ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
 
 /-- Searches for an element in the heap and returns its index. **O(n)** -/
-def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le (n+1) → (pred : α → Bool) → Option (Fin (n+1))
+def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le n → (pred : α → Bool) → Option (Fin n)
 | {tree, valid := _, wellDefinedLe := _}, pred =>
   tree.indexOf pred
 
-- 
cgit v1.2.3

