Writing an external type checker for lean

Stream: new members

[Leo Shine]

Hello,

I was thinking of trying to do this, (I had a bit of a go at doing this with MetaMath once too) Do people know the best resources for this is it this https://ammkrn.github.io/type_checking_in_lean4/title_page.html type checking in lean book? Or are there others that might be better.

[Kyle Miller]

There's also Lean4Lean https://arxiv.org/abs/2403.14064 by Mario Carneiro (mentioned in the Further reading)

I don't know any other specific resources, other than reading the Lean source code, or more general resources on type checking in general.