type checker in lean4

Stream: lean4

[Eirene Pandi]

is it reasonable to write a type checker for a small calculus in lean4? I have tried to write it in lean3 and found that many "simple" things have not implemented fully

[František Silváši]

Yes it is. You could also be a bit more specific with what issues you encountered with Lean 3, perhaps Lean 4's addressed them directly or indirectly. I will say that 'simply programming' in Lean 4 (i.e. disregarding proofs) is miles ahead of Lean 3 in terms of convenience and ergonomics.

[Henrik Böving]

You will find that right now the Lean 4 builtin libraries are certainly lacking a bit if functionality that you might expect from more evolved programming languages but since Lean is perfectly capable of interpreting itself right now I see no reason why it shouldnt be possible to interpret something simpler with it.

[Eirene Pandi]

thanks, are you aware of any snippets of code that could be useful? (not examples with proofs or really simple programs)

[Henrik Böving]

Useful in what regard? For writing a type checker for some lambda calculus no. For general programs that are done in Lean you could take a look at:

• The compiler itself
• The Lake build system
• The doc-gen4 docuemntation generator (although its mostly a Meta program for Lean 4 itself)
• Sebastian posted his AoC solutions over here https://github.com/Kha/aoc-2021/
• There is some non trivial datastructure code for stuff like binary heaps in mathlib4 as of now.

[Chris B]

Mario Carneiro wrote a metamath verifier in Lean 4, but quite a bit has changed in the last nine months (for the better). https://github.com/digama0/mm-lean4