Tutorial

This tutorial is no longer maintained. See our documentation page for more recent references.


An invitation to Coq. It is a commented interactive session which introduces basics on terms, proofs, and tactics.



Index


Authors : Gérard Huet, Gilles Kahn and Christine Paulin-Mohring
©INRIA 1999-2004 (Coq versions 7.x)
©INRIA 2004-2017 (Coq versions 8.x)
This research was partly supported by IST working group “Types”.