Passed a big milestone towards bootstrapping Lean 4 today: After grafting the old elaborator (written in C++) onto the new frontend (written in Lean) in true Frankensteinian fashion, the new frontend can now process all 2176 lines of core.lean successfully!
Conversation
Replying to
Is there a place we can go to have a sneak peek at this work? Super interested to see how one goes about implementing an elaborator for Lean in Lean. :)
Replying to
Not quite yet, unfortunately. Though rewriting the (term-level) elaborator in Lean is the one big task we haven't even started yet. Thus Frankenstein, for the time being.
1
3
Haha, no worries! I was actually attempting to look for the source code of your Lean parser in Lean the other day, but also couldn't find it either. Is that also a WIP?
1
2
Show replies