should nonempty be a structure

Stream: general

[Johan Commelin]

This came up here: https://github.com/leanprover-community/mathlib/pull/1964#discussion_r375744750
I have no idea if it is important that it is an inductive type

[Mario Carneiro]

Repeating what I said there: nonempty can't be a structure, because it doesn't have projections. It is possible to define class my_nonempty (A) : Prop := (foo : nonempty A) and now it's a structure, but this has some unusual behavior when you attach it to another structure bar A via extends. In particular, the foo projection will become a projection on bar as well, in addition to to_nonempty : bar A -> my_nonempty A.

My suggestion is to just put (to_nonempty : nonempty A) as a field on bar if you need it, and add an instance. It's not a structure.