The Coq mailing list

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

On 01/24/2014 04:35 PM, Thomas Knight wrote:
> I looked at various parts of the documentation available for Coq, and 
> I have a suggestion that would really help me.
>
> Andrej Bauer has a video showing how to do induction with natural 
> numbers and binary trees ( http://www.youtube.com/watch?v=fbt0TcLzrNg ).
>
> What would be really helpful is a set of 100 examples of that kind of 
> utility all available online.

Maybe I'm old-fashioned, but to me, 100 examples in one place, if tied 
together properly, become "a book," and there are several available on 
Coq, including on the web. ;)