coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] non instanciated existential variables

From: Pierre Casteran <casteran AT labri.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] non instanciated existential variables
Date: Mon, 09 Feb 2004 14:03:02 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: LaBRI

Hello,

How can I give some (arbitrary) values to Coq when I get such a
message ? (In this case, any nat would be OK)

Pierre

No more subgoals but non-instantiated existential variables :
Existential 1 =
?160 : [
        I : Set
        J : Set
        A : Set
        W : Set
        i : I
        decI : eqdec I
        decJ : eqdec J
        n : nat
        w : W
        F : Form I J A
        G : Form I J A
        H : Form I J A |- nat]
--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran

[Coq-Club] non instanciated existential variables, Pierre Casteran