Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Strictly positive inductive types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Strictly positive inductive types


Chronological Thread 
  • From: <elilobo.v AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Strictly positive inductive types
  • Date: Mon, 11 Aug 2014 22:54:50 +0200

How to force Coq to accept non-strictly positive inductive types? Is there a
flag like --no-positivity-check in Agda, to do it?



Archive powered by MHonArc 2.6.18.

Top of Page