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).
This commit is contained in:
parent
2e8afdf74d
commit
d4c74b3566
1 changed files with 8 additions and 0 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue