diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean index c393bbd3f1..e5e5f4ea30 100644 --- a/src/Init/Data/Ord.lean +++ b/src/Init/Data/Ord.lean @@ -12,14 +12,6 @@ inductive Ordering where | lt | eq | gt deriving Inhabited, BEq -namespace Ordering - -def lexOrdering (orderings : List Ordering) : Ordering := - orderings.foldr (init := Ordering.eq) fun ordering result => - if ordering == Ordering.eq then result else ordering - -end Ordering - class Ord (α : Type u) where compare : α → α → Ordering diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index 0cc43706e2..935e7d3f3c 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -42,10 +42,7 @@ instance : LE Position := leOfOrd structure Range where start : Position «end» : Position - deriving Inhabited, BEq, Hashable, ToJson, FromJson - -instance : Ord Range where - compare a b := Ordering.lexOrdering [compare a.start b.start, compare a.end b.end] + deriving Inhabited, BEq, Hashable, ToJson, FromJson, Ord instance : LT Range := ltOfOrd instance : LE Range := leOfOrd