Skip to Content.
Sympa Menu

coq-club - [Coq-Club] positivity check

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] positivity check


Chronological Thread 
  • From: Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] positivity check
  • Date: Mon, 18 Nov 2013 12:01:33 -0200

Hi CoqClub,

Is it possible to disable positivity checking temporarily?  I know that doing it will lead to inconsistencies, but  I just want to experiment a bit with a non strictly positive inductive type.

Thank you.




Archive powered by MHonArc 2.6.18.

Top of Page