The Coq mailing list

[Aurore Collomb <aurorecollomb AT chez.com>]

Bonjour,

Debutante dans l'utilisation de Coq me voici avec les hyotheses et le 
but suivant :
 e : expr
 e' : expr
 n : nat
 n0 : nat
 n1 : nat
 Hrec : {(Num n1)=(Num (0))}+{~(Num n1)=(Num (0))}
 a : (Num n1)=(Num (0))
 H : (Num (S n1))=(Num n1)
 H1 : (S n1)=n1
 ============================
  False

J'avais envie de lui dire que H1 n'est pas possible, mais
discriminate H1 me dit :
Error:  Not a discriminable equality

Pourtant n1 est bien un type inductif... ou est mon erreur ?

Merci

Aurore Collomb

--
INRIA - VASY
655 av. de l'Europe
F-38330 Montbonnot Saint-Martin
Tel : 04.76.61.53.37
http://www.inrialpes.fr/vasy/people/Aurore.Collomb/