This is a book about Lean 4's kernel and implementing external type checkers; it's built with mdBook.
A hosted copy can be found at https://ammkrn.github.io/type_checking_in_lean4/
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