coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Georgi Guninski <guninski AT guninski.com>
To: Jean-Francois Monin <jean-francois.monin AT imag.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?
Date: Wed, 25 May 2011 16:34:36 +0300
Header: best read with a sniffer

On Wed, May 25, 2011 at 09:30:07PM +0800, Jean-Francois Monin wrote:
> 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

thank you!

--
joro

[Coq-Club] is it normal [firstorder] to hang on simple testcase?, Georgi Guninski
- Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Pierre Corbineau
  - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Georgi Guninski
    - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Jean-Francois Monin
      - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Georgi Guninski
    - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Pierre Corbineau
      - Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Georgi Guninski
        
        Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, David Baelde
        
        Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Georgi Guninski
        
        Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, David Baelde
        
        Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Alexandre Pilkiewicz
        
        Re: [Coq-Club] is it normal [firstorder] to hang on simple testcase?, Stéphane Glondu