Post #3057014

And it's done! I did not expect to write *checks `grep | xargs wc -w` 28,000 words about dependently-typed Fizzbuzz, but here we go. Time to find a more interesting thing to work on in the evenings (debating between doing some Alive-style translation validation in Dafny and embedding LTL in Lean...) The whole series: https://ntaylor.ca/posts/proving-the-coding-interview-lean/