coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] How to prove an inductive property on trees.
- Date: Sun, 7 Feb 2016 23:42:24 +0100 (CET)
Dear Adam,
May be I am wrong but it seems to me CPDT sect 3.8 covers (non-dependent) induction over Prop,
not dependent induction over Type ? Moreover, I did not see a fixpoint equation for your recursor
nat tree ind’.
I am certainly not saying that CPDT 3.8 is not worth reading though !
Best regards,
Dominique
De: "Adam Chlipala" <adamc AT csail.mit.edu>
À: coq-club AT inria.fr
Envoyé: Dimanche 7 Février 2016 22:56:31
Objet: Re: [Coq-Club] How to prove an inductive property on trees.I do think my one-line reference to a section of CPDT almost covers the same material, perhaps with a less fancy example. ;-)
On 02/07/2016 03:59 PM, Dominique Larchey-Wendling wrote:Dear Benoit,(* sorry for the duplicate but this is the complete answer, I didsend the first one too early ... *)
- [Coq-Club] How to prove an inductive property on trees., Benoît Viguier, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Adam Chlipala, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Adam Chlipala, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Frédéric Blanqui, 02/09/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Adam Chlipala, 02/07/2016
- Re: [Coq-Club] How to prove an inductive property on trees., Dominique Larchey-Wendling, 02/07/2016
Archive powered by MHonArc 2.6.18.