This is a heavily interactive web application, and JavaScript is required. Simple HTML interfaces are possible, but that is not what this is.
Post
Chris Henson
chenson.bsky.social
did:plc:ads7pcmwsk23ngs4pfttexuy
Day 5 of #AdventofCode in Lean: https://github.com/chenson2018/advent-of-code/blob/main/2024/lean/AoC/Day05.lean
One of my favorite days so far, came out very cleanly. Having quicksort in the language is nice. I enjoyed writing the function to get the middle of an Array with a provably correct index, though ran into some decidable equality trickiness.
2024-12-05T08:32:16.013Z