The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Le 04/11/2011 03:50, Andrew Pennebaker a écrit :
> Alexandre, thanks for understanding. And SF is reading great so far. :)
>
> Christopher, I'm sorry if my tone seemed aggressive or accusatory. I
> respect that considering the problem domain, Coq's interface is
> unimaginably intuitive. The problem isn't so much Coq as the paucity of
> Coq documentation. Coq syntax is still too new to Google.
>
> What if we make a Coq Newbie mailing list? I think we'd all be happier
> if I put my piddling syntax questions there instead of clogging up the
> main mailing list.
>
> Daniel, thanks (a lot a lot) for the code examples. I understood why Coq
> didn't like my code, but I didn't know how to code it better.
>
> Cheers,
>
> Andrew Pennebaker
> www.yellosoft.us <http://www.yellosoft.us>

Hello,

  Talking about Fibonnaci sequence, recursion and all that, there is 
also a lot of exercises (with their solution) in :
http://www.labri.fr/perso/casteran/CoqArt/progav/index.html  (exercises 
9.8, 9.10, 9.15, 9.17) and
http://www.labri.fr/perso/casteran/CoqArt/gen-rec/index.html ;(exercise 15.8)

Pierre