coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
> }.
- Re: [Coq-Club] records, Arnaud Spiwack
- Re: [Coq-Club] records, AUGER Cédric
Archive powered by MhonArc 2.6.16.