diff options
| author | Andreas Grois <andi@grois.info> | 2024-07-24 14:27:43 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-07-24 14:27:43 +0200 |
| commit | 76e6405c9f810bf9830756bb20ad9e4be3214b89 (patch) | |
| tree | 2e4213ab647fb93de06231803607f6cb9f98873b | |
| parent | 484c40ac59269a2f6d6e77f81defc4067539f733 (diff) | |
Fix performance issue in CompleteTree.contains.
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalOperations.lean | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalOperations.lean b/BinaryHeap/CompleteTree/AdditionalOperations.lean index d248904..3327e70 100644 --- a/BinaryHeap/CompleteTree/AdditionalOperations.lean +++ b/BinaryHeap/CompleteTree/AdditionalOperations.lean @@ -67,13 +67,14 @@ instance {α : Type u} [DecidableEq α] {tree : CompleteTree α n} {element : α Decidable.isTrue $ Or.inl t else have hl := go p l - have hr := go q r if h₁ : hl.decide then Decidable.isTrue $ Or.inr $ Or.inl $ decide_eq_true_eq.mp h₁ - else if h₂ : hr.decide then - Decidable.isTrue $ Or.inr $ Or.inr $ decide_eq_true_eq.mp h₂ else - have h₁ : ¬l.contains element := decide_eq_true_eq.subst h₁ - have h₂ : ¬r.contains element := decide_eq_true_eq.subst h₂ - Decidable.isFalse $ not_or_intro t $ not_or_intro h₁ h₂ + have hr := go q r + if h₂ : hr.decide then + Decidable.isTrue $ Or.inr $ Or.inr $ decide_eq_true_eq.mp h₂ + else + have h₁ : ¬l.contains element := decide_eq_true_eq.subst h₁ + have h₂ : ¬r.contains element := decide_eq_true_eq.subst h₂ + Decidable.isFalse $ not_or_intro t $ not_or_intro h₁ h₂ go n tree |