This file shows how to process an HTML file with Alectryon. To compile it, use the following command:

      alectryon literate_HTML.html # HTML → HTML, produces ‘literate_HTML.annotated.html’
    

To use Alectryon with your own HTML file, just wrap your code in pre tags with the alectryon class. Here are some examples:

Require Import ZArith.
    

Goal True /\ True.
  split. (* .unfold *)
  - exact I.
    

    Check nat. (* .unfold *)
  - exact I.
Qed.