Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] records

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] records


chronological Thread 
  • From: Arnaud Spiwack <arnaud AT spiwack.net>
  • To: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
  • Cc: coq-club AT inria.fr, Nuno Gaspar <nmpgaspar AT gmail.com>
  • Subject: Re: [Coq-Club] records
  • Date: Fri, 2 Dec 2011 11:31:23 +0100

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
>     }.




Archive powered by MhonArc 2.6.16.

Top of Page