coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strictly positive inductive types

From: Luke Maurer <maurerl AT cs.uoregon.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Strictly positive inductive types
Date: Mon, 11 Aug 2014 14:04:46 -0700
Authentication-results: cranium; dmarc=none header.from=cs.uoregon.edu

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?

[Coq-Club] Strictly positive inductive types, elilobo.v, 08/11/2014
- Re: [Coq-Club] Strictly positive inductive types, Luke Maurer, 08/11/2014
  - Re: [Coq-Club] Strictly positive inductive types, Maxime Dénès, 08/11/2014
    - Re: [Coq-Club] Strictly positive inductive types, Elisabet Lobo, 08/11/2014