Expand description
§lean2md
A library for converting Lean files to Markdown with special features for documentation.
§Features
- Converts Lean comments to Markdown text
- Maintains Lean code blocks inside Markdown code fences
- Supports special markers for controlling output
- Handles quiz generation for mdbook-quiz integration
Structs§
- Block
- Represents a block of content extracted from a Lean file
Functions§
- build_
blocks - Parses a Lean file’s text into output blocks plus any quizzes.
- process_
directory - Processes a directory of Lean files and converts them to Markdown
- process_
file - Processes a single Lean file and converts it to Markdown