Slides for Tsinghua Coq Summer School
For Bordeaux students
Go to this page .
Slides in pdf (Yves Bertot, Pierre Castéran)
Programming with Coq (Y.B.)
Datatypes, pattern-matching and recursion (Y.B)
Proofs in proposition logic and first-order logic (P.C.)
Simple proofs about recursive functions (Y.B.)
Inside Coq's type system (P.C.)
Interactions between inductive and dependent types (Y.B.)
Infinite objects and proofs (P.C.)
list of exercises
Class 1
Class 2
Class 3
Class 4
Class 5
Class 6
Class 7
Links and useful information
Coq home page
Coq'Art home page
Use of Proof General (Bordeaux students)
Add to your Emacs configuration file :
.emacs
or
.xemacs/init.el
the following line:
(load "/usr/share/emacs/site-lisp/proofgeneral/generic/proof-site.el")