The Coq mailing list

[Pierre Corbineau <Pierre.Corbineau AT imag.fr>]

There is no axiom-free term of type CC (just look at the normal form it 
would have).

You can even prove it:

Inductive CC : Prop := C1: (exists B : Prop,CC)->CC.

Lemma U:CC -> False.
fix 1.
intros [[ _ H]].
apply U.
apply H.
Qed.

I would tend to interpret the segfault as a consequence of another 
unbounded recursion (undetected stack overflow).

Pierre

Le 25/05/2011 15:18, Georgi Guninski a écrit :
> On Tue, May 24, 2011 at 04:05:47PM +0200, Pierre Corbineau wrote:
> > It is a feature: AA is recognized as a 'logical connective' and is
> > 'eagerly unfolded'.
> >
> > Pierre
> thank you.
>
> is this True or False, [firstorder] crashes with SEGV and i can't prove it:
>
> Inductive CC : Prop := C1: (exists B : Prop,CC)->CC.

--
Pierre Corbineau          | 
Pierre.Corbineau AT imag.fr
VERIMAG - Centre Équation | Tel: (+33 / 0) 4 56 52 04 42
2, avenue de Vignate      | Office nr B18
38610 GIÈRES - FRANCE     | http://www-verimag.imag.fr/~corbinea/
begin:vcard
fn:Pierre Corbineau
n:Corbineau;Pierre
org;quoted-printable:Universit=C3=A9 Joseph Fourier - Grenoble 1;Laboratoire VERIMAG - Polytech' Grenoble
adr;quoted-printable;quoted-printable:2, avenue de Vignate;;VERIMAG - Centre =C3=89QUATION ;GI=C3=88RES ;;38610;France
email;internet:Pierre.Corbineau AT imag.fr
title;quoted-printable:Ma=C3=AEtre de Conf=C3=A9rences
tel;work:+33 (0) 4 56 52 04 42
tel;fax:+33 (0) 4 56 52 03 44
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~corbinea
version:2.1
end:vcard

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature