Theorem Proving in Lean 4

repository·master·Indexed 42 days ago

https://github.com/leanprover/theorem_proving_in_lean4

Source code and documentation for the book 'Theorem Proving in Lean 4', authored by Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich.

Tokens: 130
Snippets: 2
Records: 2
Agent score: 5%

What's inside Lean 4

View the built book locally
master
Once the book has been built, you can view the multi-page Web version by running the verso-serve executable from the book directory.
```
cd book
lake exe verso-serve
```
https://github.com/leanprover/theorem_proving_in_lean4/blob/master/README.md
Build the Theorem Proving in Lean 4 book
master
To build the local version of the book from source, navigate to the book directory and use the lake build tool to execute the tpil executable. The resulting multi-page HTML version will be located in book/_out/html-multi.
```
cd book
lake exe tpil
```
https://github.com/leanprover/theorem_proving_in_lean4/blob/master/README.md