issue !4#5171: Porting note: Missing has nonempty instanc...

Stream: triage

[Random Issue Bot]

Today I chose issue 5171 for discussion!

Porting note: Missing has nonempty instance linter
Created by @Ruben Van de Velde (@Ruben-VandeVelde) on 2023-06-17
Labels: enhancement, t-meta, lean4-change-in-behaviour, porting-notes, tech debt

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kyle Miller]

I remember some more discussion about this linter at some point, but here's one comment I found by Gabriel Ebner:

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/lintsprint.206.20Oct/near/212391130

The idea with the inhabited instances linter was to make sure that we have the obvious instances for inhabited (finset α), inhabited (α →₀ β), etc. (Quite a few were missing, actually.) You're not expected to add inhabited instances for α ≃ β, etc.

Some people like the linter because it reminds you to add an example value of your new type.

It used to be the inhabited instance linter back then, but in the meantime we changed it to be the nonempty instance linter because people were filling it with noncomputable instances.

[Kyle Miller]

Oh, apparently I changed it in mathlib3#15542. There's more discussion there about the original motivation for the linter, and support both for and against its presence.

[Random Issue Bot]

Today I chose issue 5171 for discussion!

Porting note: Missing has nonempty instance linter
Created by @Ruben Van de Velde (@Ruben-VandeVelde) on 2023-06-17
Labels: enhancement, t-meta, lean4-change-in-behaviour, porting-notes, tech debt

Is this issue still relevant? Any recent updates? Anyone making progress?