diff options
| author | Andreas Grois <andi@grois.info> | 2024-01-13 18:01:25 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-01-13 18:01:25 +0100 |
| commit | 212e250861f65fdddadbae1e8c79e4617ea36051 (patch) | |
| tree | 3541f9005c8ef4a623b7ead34463d51bb6d6c576 /Common | |
| parent | 44e1c40fdef5d68b076d23ee030d5914d51b1414 (diff) | |
Minor, rename wellDefinedLt to wellDefinedLe
Diffstat (limited to 'Common')
| -rw-r--r-- | Common/BinaryHeap.lean | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index 9d93c97..624caa1 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -38,7 +38,7 @@ def HeapPredicate {α : Type u} {n : Nat} (heap : CompleteTree α n) (le : α structure BinaryHeap (α : Type u) (le : α → α → Bool) (n : Nat) where tree : CompleteTree α n valid : HeapPredicate tree le - wellDefinedLt : transitive_le le ∧ total_le le + wellDefinedLe : transitive_le le ∧ total_le le /--Please do not use this for anything meaningful. It's a debug function, with horrible performance.-/ instance {α : Type u} [ToString α] : ToString (CompleteTree α n) where @@ -321,10 +321,10 @@ theorem CompleteTree.heapInsertIsHeap {elem : α} {heap : CompleteTree α o} {le exact h₁.right.right.left def BinaryHeap.insert {α : Type u} {lt : α → α → Bool} {n : Nat} : α → BinaryHeap α lt n → BinaryHeap α lt (n+1) -| elem, BinaryHeap.mk tree valid wellDefinedLt => - let valid := tree.heapInsertIsHeap valid wellDefinedLt.left wellDefinedLt.right +| elem, BinaryHeap.mk tree valid wellDefinedLe => + let valid := tree.heapInsertIsHeap valid wellDefinedLe.left wellDefinedLe.right let tree := tree.heapInsert lt elem - {tree, valid, wellDefinedLt} + {tree, valid, wellDefinedLe} /--Helper function for CompleteTree.indexOf.-/ def CompleteTree.indexOfAux {α : Type u} [BEq α] (elem : α) (heap : CompleteTree α o) (currentIndex : Nat) : Option (Fin (o+currentIndex)) := |