diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-13 20:47:08 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-13 20:47:08 +0200 |
| commit | 8bbaa53546849c018d7546772080951c45ad0c34 (patch) | |
| tree | 35b389cd55f043d3b9c976885654ecf906188ee4 /BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean | |
| parent | 4f9585b8617ecb65fb97408b831ff45ef25ad0c3 (diff) | |
Fix compilation with Lean 4.10.
Diffstat (limited to 'BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean')
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean index e99617b..487a50f 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean @@ -73,7 +73,7 @@ private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : Complete have h₄ : j = indexl.val := Nat.succ.inj $ h₃.subst (motive := λx↦ x = indexl.val + 1) h₂ have : p = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) := rfl have h₅ : j < p := by simp only [this, indexl.isLt, h₄] - simp only [h₅, ↓reduceDite, Nat.add_eq] + simp only [h₅, ↓reduceDIte, Nat.add_eq] unfold get at prereq split at prereq rename_i pp ii ll _ hel hei heq _ @@ -121,7 +121,7 @@ private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : Complete exact Nat.succ.inj h₂ have : p = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) := rfl have h₅ : ¬(j < p) := by simp_arith [this, h₄] - simp only [h₅, ↓reduceDite, Nat.add_eq] + simp only [h₅, ↓reduceDIte, Nat.add_eq] unfold get at prereq split at prereq rename_i pp ii rr _ hel hei heq _ |