Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

modified def mod_p
modified structure perfection_map
modified def pre_tilt
modified def tilt