chore: adjust DecidableRel instance for leOfOrd

2026-03-17 18:34:06 +00:00 · 2024-09-30 16:46:28 +10:00
1 changed files with 4 additions and 2 deletions
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -187,13 +187,15 @@ def lexOrd [Ord α] [Ord β] : Ord (α × β) where
 def ltOfOrd [Ord α] : LT α where
  lt a b := compare a b = Ordering.lt

-instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
+attribute [local instance] ltOfOrd in
+instance [Ord α] : DecidableRel ((· : α) < ·) :=
  inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))

 def leOfOrd [Ord α] : LE α where
  le a b := (compare a b).isLE

-instance [Ord α] : DecidableRel (@LE.le α leOfOrd) :=
+attribute [local instance] leOfOrd in
+instance [Ord α] : DecidableRel ((· : α) ≤ ·) :=
  inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))

 namespace Ord