Stream: new members
Horatiu Cheval (Feb 12 2021 at 14:10):
I've seen people discussing various components such as the kernel, the VM or the elaborator, but I don't have a clear picture of what everything does and how it fits together. Is there a place where I can learn about these things?
Bryan Gin-ge Chen (Feb 12 2021 at 16:04):
I don't know that there's a single good place to read about this, but there are a bunch of papers and presentations on the official Lean website. The more detailed papers "The Lean Theorem Prover" and "Elaboration in Dependent Type Theory" are quite out-of-date since they describe Lean 2 but might still be helpful.
Horatiu Cheval (Feb 13 2021 at 08:30):
Thanks, I checked the papers, they explained pretty much what I wanted to know. I suppose the general notions carry over from Lean 2 to the newer versions.
Last updated: May 14 2021 at 04:22 UTC