From 69202d9b732501572e1a1ebdbcd617f93cd48472 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 21 Apr 2024 23:44:18 +0200
Subject: [PATCH] fix: `ReducibilityHints.lt` (#3964)

---
 src/Lean/Declaration.lean | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index 6bfca6ab00..9fcefbbd9c 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -49,13 +49,26 @@ def ReducibilityHints.getHeightEx (h : ReducibilityHints) : UInt32 :=
 
 namespace ReducibilityHints
 
+-- Recall that if `lt h₁ h₂`, we want to reduce declaration associated with `h₁`.
 def lt : ReducibilityHints → ReducibilityHints → Bool
   | .abbrev,     .abbrev     => false
   | .abbrev,     _           => true
-  | .regular d₁, .regular d₂ => d₁ < d₂
+  | .regular d₁, .regular d₂ => d₁ > d₂
   | .regular _,  .opaque     => true
   | _,           _           => false
 
+protected def compare : ReducibilityHints → ReducibilityHints → Ordering
+  | .abbrev,     .abbrev     => .eq
+  | .abbrev,     _           => .lt
+  | .regular _,  .abbrev     => .gt
+  | .regular d₁, .regular d₂ => Ord.compare d₂ d₁
+  | .regular _,  .opaque     => .lt
+  | .opaque,     .opaque     => .eq
+  | .opaque,     _           => .gt
+
+instance : Ord ReducibilityHints where
+  compare := ReducibilityHints.compare
+
 def isAbbrev : ReducibilityHints → Bool
   | .abbrev => true
   | _       => false