Skip to content

Commit d17e4c0

Browse files
chore: weekly lints for 2025-12-22 (#234)
As identified by [this workflow](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Weekly.20linting.20log/near/564936677). --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>
1 parent a8a222e commit d17e4c0

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

Cslib/Algorithms/Lean/MergeSort/MergeSort.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -217,7 +217,6 @@ theorem mergeSort_time_le (xs : List α) :
217217
grw [merge_time]
218218
simp only [mergeSort_same_length]
219219
unfold timeMergeSortRec
220-
grw [ih1,ih2]
221220
grind
222221

223222
/-- Time complexity of mergeSort -/

0 commit comments

Comments
 (0)