The script below is a minimal example of a movie generated using the Proviola. Point to the tactics to see the proof state after executing that tactic:
Lemma simple_example: forall x, x->x.1 subgoal ============================ forall x : Type, x -> xProof. intros x H.1 subgoal x : Type H : x ============================ xexact H.Proof completed.Qed.simple_example is defined
This method does not allow the reader to interact with the material directly on the web. This still requires loading the files to a proof assistant. To use the Coq proof assistant without installing it, you might want to consider ProofWeb.
This site consists of three sections:
Comments, questions and bugs can be sent directly to me (carst 'at' cs 'dot' ru 'dot' nl), or by posting an issue in the bitbucket repository.