coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: muad <muad.dib.space AT gmail.com>
- To: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] inequality of inductive types
- Date: Sun, 15 Mar 2009 06:54:38 -0700 (PDT)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
It's possible to prove nat and bool are different. For example:
Definition P (T : Set) : Prop :=
exists x : T, exists y : T, exists z : T,
x <> y /\ x <> z /\ y <> z.
P says that this type has 3 distinct elements, that's true for nat but false
for bool.
I think it's impossible to prove that:
Inductive answer := yes | not.
is different to bool, though.
--
View this message in context:
http://www.nabble.com/inequality-of-inductive-types-tp22523222p22523432.html
Sent from the Coq mailing list archive at Nabble.com.
- [Coq-Club] inequality of inductive types, Ethan Aubin
- Re: [Coq-Club] inequality of inductive types, muad
Archive powered by MhonArc 2.6.16.