coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Could I prove ~nat==bool?

From: Claudio Sacerdoti Coen <sacerdot AT students.cs.unibo.it>
To: coq-club AT pauillac.inria.fr
Subject: Could I prove ~nat==bool?
Date: Mon, 27 Sep 1999 16:39:51 +0200

Hi,

could I prove that two "different" inductive types are not equal in Type?

example: ~nat==bool is provable? If yes, how? If no, why really?

                                                        T.I.A.
                                                        C.S.C.

--
-----------------------------------------
Real Name: Claudio Sacerdoti Coen
Address: via del Colle n.6
         S. Lazzaro di Savena (BO)
         Italy
e-mail:
sacerdot AT cs.unibo.it
-----------------------------------------

Could I prove ~nat==bool?, Claudio Sacerdoti Coen
- Re: Could I prove ~nat==bool?, Benjamin Werner