Commit 2022-07-30 06:36 14b69e9f
View on Github →refactor(tactic/lint/type_classes): change inhabited linter to nonempty linter (#15542)
The inhabited
typeclass is intended to be a default value (and computable, if one is writing programs) but many times it is filled in with a junk (and perhaps noncomputable) value to satisfy the has_inhabited_instance
linter. This commit switches to a has_nonempty_instance
linter to push contributors toward supplying a nonempty
instance instead. The linter still accepts inhabited
and unique
instances, which should be preferred over nonempty
when appropriate.