A Python package that converts Lean files into markdown.
- Install it with
$ pip install lean2md - Use it with
$ python -m lean2md <lean_src_dir> <md_tgt_dir>
For a Lean file (inside <lean_src_dir>) like this:
import Mathlib.Tactic --#
namespace Sample --#
/-!
# Title
etc etc.
-/
/- Some doc -/
def one := 1
/-!
## Subtopic
* Item 1
* Item 2
-/
def two := 2
end Sample --#A markdown file like this one will be created (inside <md_tgt_dir>):
# Title
etc etc.
Some doc
```lean
def one := 1
```
## Subtopic
* Item 1
* Item 2
```lean
def two := 2
```Note that lines ending in --# (without trailing white spaces) are ignored by lean2md.