diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-13 18:34:59 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-13 18:34:59 +0100 |
| commit | 23e44c7a421d47c71318d12b1a7c5d27fb5f393a (patch) | |
| tree | 83a5cba3132a5b21a715b359c5aabec128f4d1fe /test-suite/interactive | |
| parent | bd76e995548d23100f2dbe7f5d13047402eb8251 (diff) | |
Paral-ITP demo: better comments
Diffstat (limited to 'test-suite/interactive')
| -rw-r--r-- | test-suite/interactive/Paral-ITP.v | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/test-suite/interactive/Paral-ITP.v b/test-suite/interactive/Paral-ITP.v index 658e6856f..69d3b8b88 100644 --- a/test-suite/interactive/Paral-ITP.v +++ b/test-suite/interactive/Paral-ITP.v @@ -1,3 +1,4 @@ +(* Some boilerplate *) Fixpoint fib n := match n with | O => 1 | S m => match m with @@ -7,25 +8,34 @@ Fixpoint fib n := match n with Ltac sleep n := try (cut (fib n = S (fib n)); reflexivity). +(* Tune that depending on your PC *) Let time := 18. + +(* Beginning of demo *) + Lemma a : True. Proof. sleep time. idtac. sleep time. + (* Error, jump back to fix it, then Qed again *) exact (I I). Qed. Lemma b : True. Proof. - do 11 (cut Type; [ intro foo; clear foo | exact Type]). sleep time. idtac. sleep time. + (* Here we use "a" *) exact a. Qed. -Lemma work_here : True. +Lemma work_here : True /\ True. Proof. -exact I. +(* Jump directly here, Coq reacts immediately *) +split. + exact b. (* We can use the lemmas above *) +exact a. + |