coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Coq Dev <coqletsgo AT yahoo.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Decidable equality on PositiveSets
- Date: Wed, 21 Dec 2011 09:43:15 +0000 (GMT)
- Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=X-YMail-OSG:Received:X-Mailer:Message-ID:Date:From:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=GYgmrRpGP4ziEKnMGCpQBk21qWjs6qntbkUvDJWZ+iu7dj0rhgzcjJ55/Y+ai7al3LAPeW90JwsskoTvEead3LvK9KE7o4tNkO0afrQwgQF1TfOWak97Xpx6JFwqRBArbP6/+qLjnC91UaegxyqJFtfVThtsCboxybbqzuMemnI=;
Could someone please indicate me some texts (perhaps some basic ones) that
could help explain the following behavior?
Import MSetPositive.
Lemma l: forall (p p' : PositiveSet.t), {p = p'} + {p <> p'}.
Proof.
induction p.
Error: Cannot find the elimination combinator tree_rec, the elimination of
the inductive definition PositiveSet.tree on sort Set is probably not
allowed.
- [Coq-Club] Decidable equality on PositiveSets, Coq Dev
- Re: [Coq-Club] Decidable equality on PositiveSets, Pierre Courtieu
- Re: [Coq-Club] Decidable equality on PositiveSets, AUGER Cédric
- Message not available
- Re: [Coq-Club] Decidable equality on PositiveSets,
Damien Pous
- Re: [Coq-Club] Decidable equality on PositiveSets,
Charles D
- Re: [Coq-Club] Decidable equality on PositiveSets, AUGER Cédric
- Re: [Coq-Club] Decidable equality on PositiveSets, AUGER Cédric
- Re: [Coq-Club] Decidable equality on PositiveSets,
Charles D
- Re: [Coq-Club] Decidable equality on PositiveSets,
Damien Pous
Archive powered by MhonArc 2.6.16.