diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-26 00:18:26 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-26 00:18:26 +0200 |
| commit | a9ff650577b0b9c35066875d2dce7b4a72e0cb55 (patch) | |
| tree | 2f8915ebf9f627967ee6a5c961c5859237bf81e9 /BinaryHeap.lean | |
| parent | e47e4b79142bcee5bcdc4647dc71c7ce3954cf0b (diff) | |
Remove useless proof parameter on CompleteTree.get
Diffstat (limited to 'BinaryHeap.lean')
| -rw-r--r-- | BinaryHeap.lean | 8 |
1 files changed, 4 insertions, 4 deletions
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 |