max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: typos in Std.Classes.Ord.Basic (#9145)

Browse source 
This PR fixes two typos.
This commit is contained in:
François G. Dorais 2025-07-03 08:04:25 -04:00 • committed by GitHub
parent ff130a25a2
commit 77d79f705f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Std/Classes/Ord/Basic.lean
View file

@ -440,12 +440,12 @@ theorem LawfulBEqCmp.lawfulBEq [inst : LawfulBEqCmp cmp] [LawfulEqCmp cmp] : Law
instance LawfulBEqOrd.lawfulBEq [Ord α] [LawfulBEqOrd α] [LawfulEqOrd α] : LawfulBEq α :=
LawfulBEqCmp.lawfulBEq (cmp := compare)
instance LawfulBEqCmp.lawfulBEqCmp [inst : LawfulBEqCmp cmp] [LawfulBEq α] : LawfulEqCmp cmp where
instance LawfulBEqCmp.lawfulEqCmp [inst : LawfulBEqCmp cmp] [LawfulBEq α] : LawfulEqCmp cmp where
compare_self := by simp only [compare_eq_iff_beq, beq_self_eq_true, implies_true]
eq_of_compare := by simp only [compare_eq_iff_beq, beq_iff_eq, imp_self, implies_true]
theorem LawfulBEqOrd.lawfulBEqOrd [Ord α] [LawfulBEqOrd α] [LawfulBEq α] : LawfulEqOrd α :=
LawfulBEqCmp.lawfulBEqCmp
theorem LawfulBEqOrd.lawfulEqOrd [Ord α] [LawfulBEqOrd α] [LawfulBEq α] : LawfulEqOrd α :=
LawfulBEqCmp.lawfulEqCmp
instance LawfulBEqCmp.opposite [OrientedCmp cmp] [LawfulBEqCmp cmp] :
LawfulBEqCmp (fun a b => cmp b a) where