coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Decidable equality on PositiveSets

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, Coq Dev
- 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