The Coq mailing list

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

> As said by Adam, I am wondering if don't have confusion between 
> Records and Inductives:
Not exactly.
Inductive types are freely generated and have some initial property. 
Although this does not exist in Coq, there is probably some room for 
some kind of "freely presented" types, where constructors are given, 
together with a bunch of relations, yielding a kind of setoid with some 
initial property.

ah