coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Damien Pous <Damien.Pous AT inria.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] discriminate JMequalities
- Date: Mon, 10 Aug 2009 16:29:34 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type:content-transfer-encoding; b=paJBPbPN8L2RycfkprNjGLkxsVFJRBjMmCPUVda6I47NshtAzF78zrFYcfIUVVYHNw ZKsQ+W/cO/01T5SeigZA6WyKzhR3i95DY5oxjfgBcQpoeXMdoEBhopw2PpTAjGchXkBH eBVMYsk2zIvevjPLUWKmfQ/rSqPkMd5jiew2E=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
I am stuck with the following simple goal (even with
`standard' axioms like JMeq_eq or eq_rect_eq...).
Is there a way to solve it ?
Thanks!
Damien
Require Import JMeq.
Inductive B: bool -> Set :=
| ff: B false
| tt: B true.
Goal ~ (JMeq ff tt).
- [Coq-Club] discriminate JMequalities, Damien Pous
- Re: [Coq-Club] discriminate JMequalities,
Adam Chlipala
- Re: [Coq-Club] discriminate JMequalities,
Taral
- Re: [Coq-Club] discriminate JMequalities, Hugo Herbelin
- Re: [Coq-Club] discriminate JMequalities,
Taral
- Re: [Coq-Club] discriminate JMequalities,
Adam Chlipala
Archive powered by MhonArc 2.6.16.