Type theory pedagogic implementations in Lean 4?

Stream: lean4

[Avi Craimer]

Hi,
I have been re-watching @Jonathan Sterling giving a presentation on YouTube called How to code your own type theory. It's fantastic.

His example code is in OCaml and I wonder if somebody has written something like this in Lean? I'm not looking for a big complex implementation that would actually be useful for some practical purpose (e.g., the Lean 4 source code!). I mean something simple like what Jon shows in the presentation which is geared towards helping people learn the basics of implementing a type theory.

I also wonder if there are any beginners books or articles on the implementation of type theory. I've read a fair amount of theoretical stuff about lambda calculus and various type systems but they always gloss over the essential nitty gritty that is required to actually write code to do it, or they give code examples that are arcane and incomprehensible (to me at least).

Thanks again Jon for the great video.

[Mario Carneiro]

There is a basic type checker example in the lean manual IIRC

[Mario Carneiro]

https://lean-lang.org/lean4/doc/examples/tc.lean.html