Skip to content

Commit e11ef3e

Browse files
fix: Remove redundant instance requirement (#10941)
This PR removes a redundant instance requirement from `Std.instIrreflLtOfIsPreorderOfLawfulOrderLT`.
1 parent b2b385b commit e11ef3e

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Data/Order/Lemmas.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@ public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
110110
intro h h'
111111
exact h.2.elim h'.1
112112

113-
public instance {α : Type u} [LT α] [LE α] [IsPreorder α] [LawfulOrderLT α] :
113+
public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
114114
Std.Irrefl (α := α) (· < ·) := inferInstance
115115

116116
public instance {α : Type u} [LT α] [LE α] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) ]

0 commit comments

Comments
 (0)