The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Vladimir Voevodsky wrote:
> Is there a standard name in Coq for the following:
>
> Inductive nonempty (T:Type) : Prop := wtns: T ->  nonempty T.
>    

Yes:

Coq < Print inhabited.
Inductive inhabited (A : Type) : Prop :=  inhabits : A -> inhabited A