From c4d85b762299f69e337fc5cc3305095296d4ab8d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Feb 2026 11:46:36 -0800 Subject: [PATCH] chore: revert reducibility change `PartialOrder.rel` (#12407) This PR is similar to #12403. We previously conjectured that "all type class fields that are types should be marked as reducible." The problem is that propositions are types, but they are also used as data (with `Decidable`). For example, we often see the proposition `x <= y` as a Boolean. So, we refined the conjecture to: "All type class fields that are types (and not propositions) should be marked as reducible." --- src/Init/Internal/Order/Basic.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean index c88ff3a8ea..f47a189a50 100644 --- a/src/Init/Internal/Order/Basic.lean +++ b/src/Init/Internal/Order/Basic.lean @@ -50,8 +50,6 @@ class PartialOrder (α : Sort u) where /-- The “less-or-equal-to” or “approximates” relation is antisymmetric. -/ rel_antisymm : ∀ {x y}, rel x y → rel y x → x = y -attribute [reducible] PartialOrder.rel - @[inherit_doc] scoped infix:50 " ⊑ " => PartialOrder.rel section PartialOrder