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:

Goal True /\ True.
True /\ True
  split.
True
True
  -
True exact I.
    

    Check nat.
nat
     : Set
  -
True exact I.
Qed.