Integration with MyST

To combine Alectryon and MyST (a Markdown parser with support for docutils/Sphinx directives), just load both plugins in your Sphinx configuration:

extensions = ["alectryon.sphinx", "myst_parser"]

That’s enough to run Coq fragments and link to identifiers:

Print nat.
Inductive nat : Set :=  O : nat | S : nat -> nat.

Arguments S _%_nat_scope

For roles use {role}`argument` syntax: like this. For math use either the {math} role (\(e^{i\pi} = -1\)) or $ signs (with the dollarmath extension, see conf.py): (\(\cos(\pi) = -1\)).

Note that MyST disables MathJax’s heuristics for finding text to process (by marking the root of the document with mathjax_ignore), so any math outside of {math} or $ delimiters is not processed: \(this is not math\); use the mathjax_process HTML class to revert that.

Nesting

• Item

  Note

  • Item:

    Check nat.
    nat
         : Set

  • Item:

    • Rocq

      Check Prop.
      Prop
           : Type