Literate programming with Alectryon (Lean3 input)

Alectryon supports literate programs and documents (combinations of code and prose) written in Lean3 and reStructuredText. Here is an example written in Lean3. It can be converted to reST, HTML, or LaTeX using the following commands:

alectryon --frontend lean3+rst literate_lean3.lean
    # Lean3+reST → HTML;  produces ‘literate_lean3.html’
alectryon --frontend lean3+rst literate_lean3.lean --backend latex \
     --latex-dialect lualatex \
     -o literate_lean3.lua.tex
    # Lean3+reST → LaTeX; produces ‘literate_lean3.lua.tex’
alectryon --frontend lean3+rst literate_lean3.lean --backend rst
    # Lean3+reST → reST;  produces ‘literate_lean3.lean3.rst’

Running queries

Alectryon captures the results of #check, #eval, and the like:

#reduce let x := 5 in x + 38

By default, these results are folded and are displayed upon hovering or clicking. We can unfold them by default using annotations or directives:

#check natℕ : Type

#check boolbool : Type
#eval 1 + 12

Other flags can be used to control display, like .no-in:

structure iff : Prop → Prop → Prop
fields:
iff.mp : ∀ {a b : Prop}, (a ↔ b) → a → b
iff.mpr : ∀ {a b : Prop}, (a ↔ b) → b → a

Documenting proofs

Alectryon also captures goals and hypotheses as proofs progress:

example (p q r : Prop) : p ∧ q ↔ q ∧ p :=
  apply iff.intro,p, q, r: Prop
p ∧ q → q ∧ p
p, q, r: Prop
q ∧ p → p ∧ q {p, q, r: Prop
p ∧ q → q ∧ p
    intro H,1p, q, r: Prop
H: p ∧ q
q ∧ p
    apply and.intro,p, q, r: Prop
H: p ∧ q2
q
p, q, r: Prop
H: p ∧ q
p
    apply (and.elim_right H),p, q, r: Prop
H: p ∧ q
p
    apply (and.elim_left H),
  }, {p, q, r: Prop
q ∧ p → p ∧ q
    intro H,p, q, r: Prop
H: q ∧ p
p ∧ q
    apply and.intro,p, q, r: Prop
H: q ∧ p
p
p, q, r: Prop
H: q ∧ p
q
    apply (and.elim_right H),p, q, r: Prop
H: q ∧ p
q
    apply (and.elim_left H),
  }
end

Most features available for Coq are also available for Lean3; in particular, references (1, 2), quotes (p ∧ q) and assertions should work.

q ∧ p → p ∧ q

For now, please refer to the main README and to the Coq examples for more information.