derive LawfulBEq

leanprover · Jan 28, 2025 · 527b760 · 527b760
1 parent b05f954
commit 527b760
Showing 1 changed file with 1 addition and 8 deletions.
diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
@@ -10,17 +10,10 @@ import Init.Data.Array.Basic
 
 inductive Ordering where
   | lt | eq | gt
-deriving Inhabited, BEq
+deriving Inhabited, DecidableEq
 
 namespace Ordering
 
-deriving instance DecidableEq for Ordering
-
--- This becomes obsolete with https://github.com/leanprover/lean4/issues/5295
-instance : LawfulBEq Ordering where
-  eq_of_beq {a b} := by cases a <;> cases b <;> simp <;> rfl
-  rfl {a} := by cases a <;> rfl
-
 /-- Swaps less and greater ordering results -/
 def swap : Ordering → Ordering
   | .lt => .gt