I wrote two reference type checkers for Lean and learned a lot about both the Lean kernel and the implementation of DTT; it's not an easy exercise, but I would

I wrote two reference type checkers for Lean and learned a lot about both the Lean kernel and the implementation of DTT; it's not an easy exercise, but I would recommend it. The ones I wrote are in a language that's not the easiest to read (though I did end up getting the performance to justify the language choice), but if any related questions come up feel free to contact me and I'll do my best to give a coherent answer: https://github.com/ammkrn/nanoda_lib https://github.com/ammkrn/nanoda_lib This paper on Lean's type theory dovetails nicely with any of the kernel implementations: https://github.com/digama0/lean-type-theory/releases/tag/v1.0 https://github.com/digama0/lean-type-theory/releases/tag/v1.... Also this article is really neat, thanks OP. These kinds of visual representations and other alternative mediums you can use to document stuff are (imo) a really important and under-explored area.