TP (Coq)
Résumé de section
-
Vous trouverez dans cette section des tutos pour vous familiariser avec Coq.
Pour les essayer, vous pouvez installer Coq-Platform sur votre machine personnelle, c’est ce que nous utiliserons en TP (l’interface utilisateur s’appelle CoqIDE).
Mais vous pouvez également, si vous voulez juste faire quelques essais, utiliser un éditeur en ligne disponible à cette adresse. (il faut cliquer sur "scratchpad" pour commencer à coder).
ATTENTION : Dans les tutos, je vous indique les raccourcis claviers pour Coq Platform. Si vous utilisez l’éditeur en ligne, ils sont différents. En particulier, pour avancer dans les tactiques, il faut utiliser [Alt + ↓] et non pas [Ctrl + ↓], de même pour les autres raccourcis.
Pour commencer le TP1, il faut charger le fichier "exercices.v" dans un éditeur Coq (soit CoqIde, soit jsCoq, en ligne).
-