The Coq mailing list

[Arnaud Spiwack <arnaud AT spiwack.net>]

If I understood the question correctly, the short answer is: why should "Record" mean "Inductive" rather than "Coinductive".

A longer version would invoke history and stuff like that (and maybe a fairy or two, for the children). But to be fair, when we started taking the record notations seriously, we made the explicit choice to have "Inductive" for inductive stuff, "Coinductive" for coinductive one and "Record" for non-recursive records. The unfortunate non-uniformity here, that "Record" doesn't accept non-recursive variants is for linguistic reason and is inherited from history.

On 30 Nov 2011 14:15, "Alexandre Pilkiewicz" <alexandre.pilkiewicz AT polytechnique.org> wrote:

Inductive X: Type :=
Con {
   foo    : list nat;
   bar    : list X
   }.

will work.

I let someone else explain why it's not always the case, because I
don't really understand.

And also, I vote for a line or two about that in the documentation :-)

Alexandre


On Wed, Nov 30, 2011 at 2:09 PM, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:
> X: Type :=
> Con {
>     foo    : list Stuff;
>     bar    : list X
>     }.