The Coq mailing list

[Fr�d�ric Peschanski <Frederic.Peschanski AT lip6.fr>]

Thank you Julien,
that was exactly what I was looking for.

You did not make any mistake, only the last element
of nil is term  (for termination) ;-).

Is there somewhere a tutorial documentation on functional induction ?
(cocorico would be a nice place for such a tutorial ...).

Cheers,
Frederic.


Julien Forest a écrit :
> Dear Frederic, 
> you can use Function (to create principles) and functionnal induction (to use them).
> I've done the proofs using this technique (I needed to define hd, last and length and 
> I hope I didn't do any mistake) 
> (* I hope that this might help you. 
>    Best regards 
>    Julien Forest.
> *)
>