Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to prove an inductive property on trees.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to prove an inductive property on trees.


Chronological Thread 
  • 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 did
   send the first one too early ... *)





Archive powered by MHonArc 2.6.18.

Top of Page