TME 1 : Programmation récursive avec Coq

Configuration sur les machines de la PPTI

Pour utiliser ProofGeneral, l’interface utilisateur de haut niveau pour Coq, ajoutez à votre fichier .emacs la ligne suivante :
(load-file "/usr/local/ProofGeneral/generic/proof-site.el")

Sujet

Ouvrez le fichier suivant dans emacs, et modifiez-le en suivant les instructions :
tme01student.v

Le sujet en pdf (pour lecture) ici