Built with Alectryon, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.

Literate programming with Alectryon (Lean4 input)

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

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

Running queries

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

def x : Nat := 5

10
 5 + x

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

Nat : Type
 Nat
Bool : Type
 Bool

2

 1 + 1

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

inductive Iff : Prop → Prop → Prop
number of parameters: 2
constructors:
Iff.intro : ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
 Iff

Documenting proofs

Alectryon also captures goals and hypotheses as proofs progress:

theorem test (p q : Prop) (hp : p) (hq : q): p ∧ q ↔ q ∧ p := 
p, q: Prop
hp: p
hq: q
p ∧ q ↔ q ∧ p

  
p, q: Prop
hp: p
hq: q
mp
p ∧ q → q ∧ p
p, q: Prop
hp: p
hq: q
q ∧ p → p ∧ q

  
p, q: Prop
hp: p
hq: q
mp
p ∧ q → q ∧ p
 
p, q: Prop
hp: p
hq: q
h: p ∧ q
mp
q ∧ p

    
p, q: Prop
hp: p
hq: q
h: p ∧ q
mp.left
q
p, q: Prop
hp: p
hq: q
h: p ∧ q
p

    
p, q: Prop
hp: p
hq: q
h: p ∧ q
mp.left
q
 
Goals accomplished! 🐙

    
p, q: Prop
hp: p
hq: q
h: p ∧ q
mp.right
p
 
Goals accomplished! 🐙

  
p, q: Prop
hp: p
hq: q
mpr
q ∧ p → p ∧ q
 
p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr
p ∧ q

    
p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.left
p
p, q: Prop
hp: p
hq: q
h: q ∧ p
q

    
p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.left
p
 
Goals accomplished! 🐙

    
p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.right
q
 
Goals accomplished! 🐙