The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

Le Tue, 26 Oct 2010 10:37:29 -0400,
Vladimir Voevodsky 
<vladimir AT ias.edu>
 a écrit :

> Hello,
> 
> could someone tell me where I can find the conditions which the
> constructors of co-inductive types in Coq should satisfy? In the
> inductive case there is the positivity condition, what are the
> co-inductive conditions?
> 
> Thanks!
> Vladimir. 

I may be wrong, but I believe that the conditions are exactly the same.
The differences are on the use of them and what they define.
Maybe a quick look in the coq source may help you to see if same
checking functions are called.

I checked that a positivity condition was also required in CoInductive:

CoInductive t: Prop := A: ~t -> t.

Inductive is the smallest type linked to its constraints and coinductive
is the biggest one (to the same constraints).