How a LeanBlog post is built
Source model
A post travels through three small layers. PostSource is the source
model from the Markdown module. Its toPart method lowers the
parsed body into the Verso blog representation after every lean: destination has been resolved.
Parsing source
Markdown becomes a small, explicit source model before any theme code runs. This keeps authoring errors close to the input file and makes the later rendering stages easier to test.
Lowering to Verso
The parsed body is lowered only after declaration destinations have been resolved, so links and content travel together into the generated post.
Declaration links
The link registry lives in a separate module. A DeclarationIndex
maps a Lean name to one or more Target values. That separation means a
future frontend can reuse the same links without knowing anything about Markdown.
Registry boundary
The registry stores resolved targets while Markdown remains responsible for syntax. The boundary is deliberately small: a frontend asks for a target and receives a normal URL.
Source files and themes
Here is the shape of a source file:
--- title: A post date: 2026-08-06 authors: Jonathan Prieto-Cubides --- The [`Target`](lean:LeanBlog.Target) is a generated link.
The theme stays at the edge. Theme.make receives the compiled CSS and
hands Verso the page templates, so writing content does not require learning the HTML template API.
Lean examples
The same post can include an ordinary Lean example:
def greeting : String := "LeanBlog"
#eval greeting