Writing Alectryon documents in Markdown with MyST

To compile this file, use one of the following commands:

$ alectryon literate_MyST.md
  # MyST → HTML, produces ‘literate_MyST.html’

$ alectryon literate_MyST.md --backend coq
  # MyST → Coq, produces ‘literate_MyST.v’

Alectryon supports input files written in MyST (a Markdown variant) in addition to Coq and reStructuredText.

In MyST Coq fragments are spelled as ```{coq}, with arguments on the same line and options below:

Goal exists x, x * x = 49 /\ x < 10.
exists x : nat, x * x = 49 /\ x < 10
  let rec t n := (exists n; split; [reflexivity |]) || t (S n) in t 0.
7 < 10
  unfold lt.
8 <= 10
  repeat constructor.

Math is written either in Docutils math roles (\(e^{i\pi} = -1\)) or in $ signs with option dollarmath (see docutils.conf in this directory: \(\cos(\pi) = -1\)). And unlike in reST, built-in inline markup nests, including code and other roles like coqid references or links.