The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

I'm almost sure this has already been discussed here, but I can't find
it anymore, so I'm asking before doing anything wrong.

Here is my problem: is there something subtle I'm missing between the
two following (co)inductive definitions, or is this, as I think I read
somewhere, a unimplemented feature?

This works:

Inductive toto :=
| Toto : (unit -> toto) -> toto.

This does not, because Coq asserts it would break the positivity condition:

Inductive titi :=
| Titi : (forall p, match p with tt => titi end) -> titi.

This seems really odd to me. Is there any metatheoretical result
forbidding this or may I already write the patch fixing this (which I
badly need and did not manage to somehow bypass when working with
coinductives)?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature