Skip to content

Commit 2ee7c69

Browse files
committed
fix: import the deprecated Sorted in MergeSort as temporary measure to fix compilation
1 parent 13bcebb commit 2ee7c69

2 files changed

Lines changed: 1 addition & 2 deletions

File tree

Cslib/Algorithms/Lean/MergeSort/MergeSort.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import Cslib.Algorithms.Lean.TimeM
88
import Mathlib.Data.Nat.Cast.Order.Ring
99
import Mathlib.Data.Nat.Lattice
1010
import Mathlib.Data.Nat.Log
11+
import Mathlib.Deprecated.Sort
1112

1213

1314
/-!
@@ -126,7 +127,6 @@ For a list of length `n`, this counts the total number of comparisons:
126127
- Base cases: 0 comparisons for lists of length 0 or 1
127128
- Recursive case: split the list, sort both halves,
128129
then merge (which takes at most `n` comparisons) -/
129-
130130
def timeMergeSortRec : ℕ → ℕ
131131
| 0 => 0
132132
| 1 => 0

Cslib/Algorithms/Lean/TimeM.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,6 @@ namespace Cslib.Algorithms.Lean
3636
/-- A monad for tracking time complexity of computations.
3737
`TimeM α` represents a computation that returns a value of type `α`
3838
and accumulates a time cost (represented as a natural number). -/
39-
4039
structure TimeM (α : Type*) where
4140
/-- The return value of the computation -/
4241
ret : α

0 commit comments

Comments
 (0)