Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Decidable equality on PositiveSets

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Decidable equality on PositiveSets


chronological Thread 
  • 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.





Archive powered by MhonArc 2.6.16.

Top of Page