The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

Le 11/08/2014 23:23, Maxime Dénès a écrit :

Coq does reject non strictly positive types, even if they are positive. Otherwise it would be inconsistent in general, as you could encode the argument given in [1].

Non-strictly positive types are not necessarily inconsistent. In Inductively defined types, COLOG'88, Thierry Coquand and Christine Paulin show that a particular "big" non-strictly positive type is inconsistent (section 3.1, page 59). I call it "big" for it has a constructor having a type argument that is not a parameter. The constructor has type ((X->Prop)->Prop)->X. However, "small" (e.g. replace Prop by bool) non-strictly positive types are harmless.

Best regards,

Frédéric.

I don't know of any flag to disable this check but a patch should not be too hard to write. What's your use case?

Maxime.

[1] A new paradox in type theory, T. Coquand - Proceedings 9th Int. Congress of Logic, Methodology, 1991

On 08/11/2014 05:04 PM, Luke Maurer wrote:

AFAIK, Coq always accepts types that are positive but not strictly so. And it never accepts non-positive occurrences (unlike with Agda, Coq's termination checking is mandatory).

- Luke

On Aug 11, 2014, at 1:54 PM, <elilobo.v AT gmail.com> wrote:

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