(* Some boilerplate *) Fixpoint fib n := match n with
| O => 1
| S m => match m with
| O => 1
| S o => fib o + fib m endend.
Ltac sleep n := try (cut (fib n = S (fib n)); reflexivity).
(* Tune that depending on your PC *) Lettime := 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.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
