chore(logic/equiv/basic): remove nolint (#15329)

leanprover-community · Jul 15, 2022 · 11bfd9c · 11bfd9c
1 parent 6f48d95
commit 11bfd9c
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/src/logic/equiv/basic.lean b/src/logic/equiv/basic.lean
@@ -69,7 +69,6 @@ universes u v w z
 variables {α : Sort u} {β : Sort v} {γ : Sort w}
 
 /-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
-@[nolint has_inhabited_instance]
 structure equiv (α : Sort*) (β : Sort*) :=
 (to_fun    : α → β)
 (inv_fun   : β → α)