[d_christiansen]

Thanks for the links! If Haskell is more your style than Racket, there's a Haskell version of the implementation tutorial at https://davidchristiansen.dk/tutorials/implementing-types-hs... .

[nequo]

The Strange Loop talk was very enjoyable. You are a gifted public speaker. And I just want to say that I am excited to read your book on Lean in full, too!