The Coq mailing list

[André Hirschowitz <ah AT unice.fr>]

> > Not exactly.
> > Inductive types are freely generated and have some initial property.
>
> Do you mean the [inductive_type]_rec, [inductive_type]_rect and so on...
> You are right, I forgot to mention it, but you can define them manually
> with fixpoints.
>
> So the solution using
> "Inductive I1 T := makeI1 : forall (x0 x1 : T), x0 = x1 -> I1 T."
> will generate them (but are trivial here).
I am not so happy with that example, let me propose a hopefully more 
enlightening one:

you want to define
Z/2Z. So you would like to write for instance

Inductive Ztwo : Type :=
O :Ztwo
| S : Ztoo ->Ztwo

WITH  forall n :Ztwo ,  SSn =n.

This corresponding  Ztwo_rect (or fixpoint) should generate a proof 
obligation for checking that the recursive formulas are compatible with 
the relations specified under the WITH banner.

ah