Commit 70551b7b authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

adapt to a september-till-december course

parent 64afe919
......@@ -20,7 +20,7 @@ The coq source files are always named with `.v` as extension (for "vernacular"..
After launch, both `coqide` and `proofgeneral` and `jsCoq` provide interfaces with a similar layout : the file being edited is in the left half of the screen, while proofs in progress are in right top and system messages are in right bottom (Coq answers, error messages, etc).
In the source file, colors are used to indicate which part of the file has already been processed by Coq, and this colored zone will grow when we send more phrases to Coq. Conversely the colored zone may also shrink if we "undo" and get Coq back to some earlier state.
Until January, we will mostly use the following commands:
For now, we will mostly use the following commands:
* `Definition` : binds some name with a (non-recursive) Coq term
* `Fixpoint` : same, for a recursive definition
......
......@@ -19,7 +19,7 @@ Par convention, les fichiers Coq utilisent l'extension `.v` (pour "vernaculaire"
Une fois lancées, les interfaces `coqide`, `proofgeneral` et `jsCoq` proposent une disposition assez similaire : le fichier en cours d'édition est à gauche, tandis que les preuves en cours seront affichées en haut à droite, et les messages du système en bas à droite (réponses de Coq ou messages d'erreurs). La portion du fichier déjà soumise à Coq est indiquée par des couleurs, et ces interfaces permettent de faire descendre cette zone, en envoyant une ou plusieurs phrases à Coq, ou au contraire de remonter (retour à un ancien état de Coq).
Dans ce cours nous allons essentiellement utiliser les commandes suivantes:
Pour l'instant, nous allons essentiellement utiliser les commandes suivantes:
* `Definition` : associe un nom à un terme Coq (non-récursif)
* `Fixpoint` : idem pour une définition récursive
......
......@@ -109,7 +109,7 @@ Definition check_invariant2 e stk :=
Compute check_invariant2 example_expr [].
Compute check_invariant2 example_expr [1;2;3;4].
(* As a teaser, the actual Coq proof. More on that in January *)
(* As a teaser, the actual Coq proof. More on that later *)
Lemma exec_prog_app p p' stk :
exec_prog (p++p') stk = exec_prog p' (exec_prog p stk).
......
......@@ -20,7 +20,7 @@ The coq source files are always named with `.v` as extension (for "vernacular"..
After launch, both `coqide` and `proofgeneral` and `jsCoq` provide interfaces with a similar layout : the file being edited is in the left half of the screen, while proofs in progress are in right top and system messages are in right bottom (Coq answers, error messages, etc).
In the source file, colors are used to indicate which part of the file has already been processed by Coq, and this colored zone will grow when we send more phrases to Coq. Conversely the colored zone may also shrink if we "undo" and get Coq back to some earlier state.
Until January, we will mostly use the following commands:
For now, we will mostly use the following commands:
* `Definition` : binds some name with a (non-recursive) Coq term
* `Fixpoint` : same, for a recursive definition
......
......@@ -19,7 +19,7 @@ Par convention, les fichiers Coq utilise l'extension `.v` (pour "vernaculaire"..
Une fois lancées, les interfaces `coqide`, `proofgeneral` et `jsCoq` proposent une disposition assez similaire : le fichier en cours d'édition est à gauche, tandis que les preuves en cours seront affichées en haut à droite, et les messages du système en bas à droite (réponses de Coq ou messages d'erreurs). La portion du fichier déjà soumise à Coq est indiquée par des couleurs, et ces interfaces permettent de faire descendre cette zone, en envoyant une ou plusieurs phrases à Coq, ou au contraire de remonter (retour à un ancien état de Coq).
Dans ce cours nous allons essentiellement utiliser les commandes suivantes:
Pour l'instant, nous allons essentiellement utiliser les commandes suivantes:
* `Definition` : associe un nom à un terme Coq (non-récursif)
* `Fixpoint` : idem pour une définition récursive
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment