The Coq mailing list

[Thomas Knight <tom1vuu2011 AT gmail.com>]

Hi everyone,

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.

In the video he mentions some particularly useful tactics for that specific application, and that kind of practical advice would allow me to use Coq properly as a proof tool.

I hope you can do this.


Thanks


Tom