I've been doing advent of code in Lean this year. It's been fun, but yeah the documentation is still a WIP. I've been searching the lean code base (I leave it

I've been doing advent of code in Lean this year. It's been fun, but yeah the documentation is still a WIP. I've been searching the lean code base (I leave it in a separate editor window) and Zulip to figure out how to do stuff. The editor support is quite interesting, and the live updates of #eval statements have helped. I look forward to finding time to do a deeper dive into the language.