The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

thank you all for the replies!

what is the human explanation of the "anything" class (i naiively would 
expect it to be close to your lemma False_ind, may be wrong).

is any of these types empty or not (the wizard can't prove it any way):

Inductive AA : Prop := A0: BB->AA with BB : Prop := B0: AA->BB .

(suppose expressing disequation won't be possible).

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].
> 
> >Lemma l1: anything.
> >Proof.
> >constructor 1.
> >(* this passes without plug-ins *)
> 
> So would running [idtac].  The problem is that you haven't finished
> the proof. :P