The Coq mailing list

[Elisabet Lobo <elilobo.v AT gmail.com>]

Thanks, I'm starting a research about inductive types and I needed
the information for general purpose.
- Elisabet Lobo-Vesga


On Mon, Aug 11, 2014 at 4:23 PM, Maxime Dénès 
<mail AT maximedenes.fr>
 wrote:
> 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].
>
> 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?
>
>