From e6b3202df3076b005b5a4a83f643be008acca18b Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 23 Feb 2023 16:37:26 -0800
Subject: [PATCH] chore: remove dead code

---
 src/Lean/Data/Name.lean | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 21b098d19b..825c3b0ea6 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -96,16 +96,6 @@ def quickCmp (n₁ n₂ : Name) : Ordering :=
 def quickLt (n₁ n₂ : Name) : Bool :=
   quickCmp n₁ n₂ == Ordering.lt
 
-/-- Alternative HasLt instance. -/
-@[inline] protected def hasLtQuick : LT Name :=
-  ⟨fun a b => Name.quickLt a b = true⟩
-
-@[inline] def Name.decLt : DecidableRel (@LT.lt Name Name.hasLtQuick) :=
-  inferInstanceAs (DecidableRel fun a b => Name.quickLt a b = true)
-
-instance : DecidableRel (@LT.lt Name Name.hasLtQuick) :=
-  Name.decLt
-
 /-- The frontend does not allow user declarations to start with `_` in any of its parts.
    We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
 def isInternal : Name → Bool