This is a book about Lean 4's kernel and implementing external type checkers; it's built with mdBook.
Users can build and view the book locally in their browser by installing mdbook and running:
mdbook watch --open # opens the output in `out/` in your default browser