Zulip Chat Archive

Stream: new members

Topic: nolint

Alex Zhang (Jul 09 2021 at 19:51):

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 (Jul 09 2021 at 19:53):

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 (Jul 09 2021 at 19:53):

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

Bryan Gin-ge Chen (Jul 09 2021 at 19:54):

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

Last updated: Dec 20 2023 at 11:08 UTC