diff options
| author | Andreas Grois <andi@grois.info> | 2025-01-13 23:32:16 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-01-13 23:32:16 +0100 |
| commit | c6e82da892f8ee79881a8dafa3c01f7c7a682ae5 (patch) | |
| tree | c9e0cbeb5ac8bf48fce53dc8fea32076e1a2e5b7 | |
| parent | 55c2353f7c209538f1421d5775afd38e6d2f0e6a (diff) | |
Minor
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapOperations.lean | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index e70ff77..6a8f190 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -40,8 +40,9 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : simp_arith[p] have right_is_power_of_two : (m+1).isPowerOfTwo := if s : n = m then - s.subst (motive := λx ↦ (x+1).isPowerOfTwo ∨ (m+1).isPowerOfTwo) subtree_complete - |> (or_self _).mp + match subtree_complete with + | .inl h₂ => (congrArg Nat.succ s).subst h₂ + | .inr h₂ => h₂ else if h₁ : leftIsFull then by rewrite[Decidable.not_and_iff_or_not (p := m<n) (q := leftIsFull)] at r cases r |