From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/interactive/ParalITP.v | 47 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 test-suite/interactive/ParalITP.v (limited to 'test-suite/interactive/ParalITP.v') diff --git a/test-suite/interactive/ParalITP.v b/test-suite/interactive/ParalITP.v new file mode 100644 index 00000000..a96d4a5c --- /dev/null +++ b/test-suite/interactive/ParalITP.v @@ -0,0 +1,47 @@ +(* Some boilerplate *) +Fixpoint fib n := match n with + | O => 1 + | S m => match m with + | O => 1 + | S o => fib o + fib m end end. + +Ltac sleep n := + try (cut (fib n = S (fib n)); reflexivity). + +(* Tune that depending on your PC *) +Let time := 18. + + +(* Beginning of demo *) + +Section Demo. + +Variable i : True. + +Lemma a : True. +Proof using i. + sleep time. + idtac. + sleep time. + (* Error, jump back to fix it, then Qed again *) + exact (i i). +Qed. + +Lemma b : True. +Proof using i. + sleep time. + idtac. + sleep time. + (* Here we use "a" *) + exact a. +Qed. + +Lemma work_here : True /\ True. +Proof using i. +(* Jump directly here, Coq reacts immediately *) +split. + exact b. (* We can use the lemmas above *) +exact a. +Qed. + +End Demo. \ No newline at end of file -- cgit v1.2.3