A LeanBlog post
Source metadata
This starter is a real .lean.md post: front matter becomes the archive metadata, and the body is
lowered to Verso's blog document model. The PostSource value keeps
the title, date, authors, and parsed Markdown together.
Linked declarations
The important part is that links stay ordinary Markdown. This one resolves through the generated Verso cross-reference index and becomes a link to the declaration page:
Lean examples
Lean examples use a fenced lean block and receive Verso's syntax highlighting:
def greeting : String := "LeanBlog"
#eval greeting
Building a collection
Build one file while writing, or point the same command at site/posts to render the whole
collection. A normal external link works too: Verso.
External declarations
For declarations documented outside this project, use a targets.tsv override. Local declarations
from the generated API do not need a hand-maintained registry.