Lean from the Inside: why I'm writing this
I use Lean for proofs about program analyses, but I learned it by imitation: copy a proof that works, change it until it works for my problem. This series is where I slow down and learn what is actually happening, from the type theory up through the elaborator, the tactics and the kernel.
The posts are notes for my future self first. If they help someone else, good.
How to read the code
Every code block here is elaborated by Lean when the site is built, so if an example stops working on a new toolchain, the build breaks and I fix the post. Hover over any identifier to see its type, and over a tactic to see the proof state.
The toolchain is pinned. This is the version every post was checked against until a later post says otherwise:
"4.32.2"#eval Lean.versionString
"4.32.2"What's coming
The series page has the roadmap. Short log entries will appear between the longer posts whenever something surprises me.