Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?


chronological Thread 
  • From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
  • To: Georgi Guninski <guninski AT guninski.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?
  • Date: Wed, 25 May 2011 21:30:07 +0800
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:in-reply-to:user-agent; b=VIqQLlNjapkJ+qUm2535P25Qmp3ZHIbpV7Xbd/V47sPL2XFlqXfuaiTRdMUxALZ6aR lTGrSyFmr+h0TwJHFVcp6bWMMa6OA+EAU8fWzey+UUqrzRQSsED2xr8FoVbZrAASfRdU lQHI3l5hZIas+nE6eZJB4pkKXYnUHkTIIt4eA=
On Wed, May 25, 2011 at 04:18:37PM +0300, Georgi Guninski wrote:
> is this True or False, [firstorder] crashes with SEGV and i can't prove it:
> 
> Inductive CC : Prop := C1: (exists B : Prop,CC)->CC.

Theorem CC_False : CC -> False.
Proof.
fix 1.
intros ((_, c)); exact (CC_False c).
Qed.


JF


Archive powered by MhonArc 2.6.16.

Top of Page