The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Andrew Pennebaker wrote:
> I rewrote fib as:
>
> Fixpoint fib (n : nat) : nat :=
> match n with
> | O => O
> | S O => one
> | _ => plus (fib (minus n one)) (fib (minus n two))
> end.
>
> Now the error is
>
> Error:
> Recursive definition of fib is ill-formed.

Your question prompted me to consider whether I'd made a crucial point 
clear enough early in CPDT.  What do you think of the explanation in the 
middle paragraph of page 19 in the latest PDF?
   http://adam.chlipala.net/cpdt/cpdt.pdf

On a more meta level, I think a good fraction of the coq-club 
participants will get annoyed if you keep using the list to ask this 
level of basic question.  I personally have some motivation to make sure 
I'm not leaving information out of CPDT, so let's tentatively say you 
can e-mail such questions to me, and I'll often just reply "that's in 
CPDT." ;-)  (And this offer only holds if you're reading through CPDT; I 
can't tell if you've decided to switch to Software Foundations as a 
substitute.)  Others might volunteer similarly.