The Coq mailing list

[Lauri Alanko <la AT iki.fi>]

On Thu, May 19, 2011 at 11:41:55AM -0400, Adam Chlipala wrote:
> Georgi Guninski wrote:
> >what is the formal definition of "empty"
> 
> A type [T] is empty if you can prove [T -> False].

Sorry to nitpick, but the above might be a bit confusing to someone
unfamiliar with the concept. Surely the formal (intensional)
definition of "empty" is that a type [T] is empty if there are no
closed terms [t] such that [t : T]?  Only due to the consistency of
Coq is this (extensionally) equivalent with your definition above.


Lauri