The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Kenneth,

 

I don't want to solve them with google, I do want to understand them. I'm just looking for pointers in how to move forward. To be able to use Coq, I need to be able to understand how to get it to see that the function will terminate, not how to solve the problem itself.

 

I am sorry, my comment was not clear. In no way I wanted to question your intentions. I just wanted to note that when it gets into more detail, it might be better to discuss it with private mail. I would think preparing this course material and good exercises has been a lot of work. I guess the authors did this mostly for their own teaching, but have been so generous to post it for public use. I think we should say thank you to the authors by ensuring that their course material and exercises remains useful for their own teaching purpose, which means we should make sure that others cannot easily solve the exercises with google.

 

Others helped me quite a bit in learning Coq and I would like to give something back in helping others in turn. But as I said, as a sign of respect for the authors of the course material I would prefer to do this by private mail (unless one of the authors encourages open discussion of their exercises).

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928