fix(library/init/data/setoid): fix redundant parameter
`setoid.refl` has two instances of `setoid A` in it
This commit is contained in:
parent
aac833c8d4
commit
316d67c3be
1 changed files with 2 additions and 4 deletions
|
|
@ -14,11 +14,9 @@ instance setoid_has_equiv {α : Sort u} [setoid α] : has_equiv α :=
|
|||
⟨setoid.r⟩
|
||||
|
||||
namespace setoid
|
||||
variable {α : Sort u}
|
||||
variable [s : setoid α]
|
||||
include s
|
||||
variables {α : Sort u} [setoid α]
|
||||
|
||||
@[refl] lemma refl [setoid α] (a : α) : a ≈ a :=
|
||||
@[refl] lemma refl (a : α) : a ≈ a :=
|
||||
match setoid.iseqv α with
|
||||
| ⟨h_refl, h_symm, h_trans⟩ := h_refl a
|
||||
end
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue