Type Checking in Lean 4

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