coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq Tutorial

From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq Tutorial
Date: Fri, 12 Aug 2016 10:26:17 +1000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f46.google.com
Ironport-phdr: 9a23:GPPVZxWmMwNdFChLaiK/hifEZTTV8LGtZVwlr6E/grcLSJyIuqrYZhKEt8tkgFKBZ4jH8fUM07OQ6PG5HzRQqs3Q+DBaKdoXBkdD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2asc272qiI9oHJZE0Q3XzmMOo0dEX99lSZ9pFPx9AzcuBpklqBi0ALUtwe/XlvK1OXkkS0zeaL17knzR5tvek8/dVLS6TwcvdwZ7VZCDM7LzJ9v5Wz5lGQBTeIs3AbSyAdlgdCKwnD9hDzGJnr4QXgse8o3TSZMNb2Baw1Rj247u8/TQLrhTwHKz8m+XvWzM1xjb5eiB2krh17hYXTZdfGZ7JFYqrBcIZCFiJ6VcFLWnkZDw==

Hi Gergely,

The tutorial is using Coq 8.2 while current version of Coq is 8.5. I am not expert in Coq, but I have a quick look at the pdf, and I think it will work with version 8.5 also. You can try software-foundations [1] and cpdt [2] for learning Coq as suggested by James.

Best regards,

Mukesh Tiwari

[1] https://www.cis.upenn.edu/~bcpierce/sf/current/
[2] http://adam.chlipala.net/cpdt/

On Thu, Aug 11, 2016 at 8:03 PM, Gergely Buday <gbuday AT gmail.com> wrote:

Hi,

I see

https://coq.inria.fr/tutorial/

as an interactive tutorial

and

http://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf

as a printable one. Is the latter up-to-date? If not, is there one to download and print?

- Gergely

[Coq-Club] Coq Tutorial, Gergely Buday, 08/11/2016
- Re: [Coq-Club] Coq Tutorial, James Smith, 08/11/2016
- Re: [Coq-Club] Coq Tutorial, mukesh tiwari, 08/12/2016