Differences

This shows you the differences between two versions of the page.

--- ingenierie_de_la_preuve [2010/06/03 22:18]
2a01:e35:8a04:6650:224:21ff:fee4:3d0a created
+++ ingenierie_de_la_preuve [2019/03/11 15:09] (current)
@@ Line 1: / Line 1: @@
-à compléter
+ == coq ==
+ Il faut installer à la fois coq et coqide (l'interface graphique pour coq).
+ Attention il se peut que les raccourcis par défaut dans coqide soient en conflit avec des raccourcis pour changer de session dans les terminaux X.
+ Pour tester il faut lancer coqide et copier-coller :
+   Lemma essai : forall A B,
+   A /\ B -> B /\ A.
+   Proof.
+   intros.
+   tauto.
+   Qed.
+ Placer le curseur sur tauto et appuyer sur le raccourci qui apparait dans le menu "navigation" pour la commande "Go to" (ctrl-alt- flèche vers la droite à priori).
+ Logiquement le texte jusqu'à tauto doit passer en vert.
+{{:snapshot-coqide.png|}}
+ Si il y a un changement de session X c'est qu'il y a un conflit avec les raccourcis de coqide.

WikiUFR Math-Info