Full description
A library to process Coq and Lean snippets embedded in text documents,
showing goals and messages for each input sentence. Also a literate
programming toolkit. The goal of Alectryon is to make it easy to write
textbooks, blog posts, and other documents that mix interactive proofs and
prose.
Alectryon originally supported Coq only. Support for Lean is preliminary
and restricted to Lean 3.
Packages