Skip to content

Lean-zh/tp-lean-zh

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Theorem Proving in Lean 4

This manual is generated by mdBook. We are currently using a fork of it for the following additional features:

  • Add support for hiding lines in other languages #1339
  • Replace calling rustdoc --test from mdbook test with ./test

To build this manual, first install the fork via

cargo install --git https://github.com/leanprover/mdBook mdbook

Then use e.g. mdbook watch in the root folder:

mdbook watch --open  # opens the output in `out/` in your default browser

Run mdbook test to test all lean code blocks.

How to deploy

./deploy.sh