The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Thu, 11 Oct 2007 19:30:10 +0200, Pierre Courtieu
<pierre.courtieu AT cnam.fr>
 a écrit:
> Interesting things are foo_equation, which is the fixpoint equation of
> foo, and the 3 induction principles foo_ind foo_rec foo_rect that
> correspond to the recursive structure of foo and are used by functional
> induction.

I should add that there is an (even more) experimental tactic
"functional inversion", due to Julien Forest (who is with Yves Bertot
the main author of all this "functional" things) which is also very
useful. Documentation in svn trunk.

P.