diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-26 19:07:36 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-26 19:07:36 +0200 |
| commit | 3bdc50ac878c1b6d066a342d2b4909b1b4e841d9 (patch) | |
| tree | 7c3faeb992f4bc3a7dfe0204d3803af25c6d8827 | |
| parent | a9ff650577b0b9c35066875d2dce7b4a72e0cb55 (diff) | |
Minor
| -rw-r--r-- | BinaryHeap.lean | 4 |
1 files changed, 2 insertions, 2 deletions
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 |