nolint

Stream: new members

[Alex Zhang]

In the mathlib, why is @[nolint has_inhabited_instance] added before the def of equiv?

@[nolint has_inhabited_instance]
structure equiv (α : Sort*) (β : Sort*) :=
(to_fun    : α → β)
(inv_fun   : β → α)
(left_inv  : left_inverse inv_fun to_fun)
(right_inv : right_inverse inv_fun to_fun)

[Bryan Gin-ge Chen]

The nolint attribute is used to disable a linter which checks to see if new types have an inhabited instance. You can read more about the linters here: https://leanprover-community.github.io/mathlib_docs/commands.html#linting%20commands

[Kevin Buzzard]

One could instead make an instance of equiv empty empty and stop it complaining :-)

[Bryan Gin-ge Chen]

There's also some information about the linters in this paper: https://arxiv.org/abs/2004.03673