From d4c74b356666e6fa713527f63abedbf4d9bd72ae Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 27 Jan 2026 06:42:30 +0100 Subject: [PATCH] fix: missing order instances for `Int` (#12181) This PR adds two missing order instances for `Int`. As reported on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/No.20Std.2EMaxOrEq.20Int.20instance.2C.20but.20yes.20Std.2EMinOrEq.20Int/near/570198709). --- src/Init/Data/Int/Order.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Init/Data/Int/Order.lean b/src/Init/Data/Int/Order.lean index 7aa1f23ed3..b68238129b 100644 --- a/src/Init/Data/Int/Order.lean +++ b/src/Init/Data/Int/Order.lean @@ -1447,4 +1447,12 @@ instance : LawfulOrderLT Int where lt_iff := by simp [← Int.not_le, Decidable.imp_iff_not_or, Std.Total.total] +instance : LawfulOrderLeftLeaningMin Int where + min_eq_left _ _ := Int.min_eq_left + min_eq_right _ _ h := Int.min_eq_right (le_of_lt (not_le.1 h)) + +instance : LawfulOrderLeftLeaningMax Int where + max_eq_left _ _ := Int.max_eq_left + max_eq_right _ _ h := Int.max_eq_right (le_of_lt (not_le.1 h)) + end Int