I did advent of code in Lean4 in 2022 and Idris2 in 2021. Lean4 was fairly similar to Idris code-wise. Minor differences: - On the Lean side I leveraged the f

I did advent of code in Lean4 in 2022 and Idris2 in 2021. Lean4 was fairly similar to Idris code-wise. Minor differences: - On the Lean side I leveraged the fact that Arrays can mutate in place (if the refcount is 1). For Idris I'd use a Buffer (IO Monad) or SortedMap. - Lean has a nice mechanism where I can drop an #eval or #check in the code and have the result show up in an editor pane. For most days, I never compiled/ran the code separately. - Lean defaults to total, so I had to put partial in a couple of places.[1] - Lean could have accepted proofs that my indices were in range, but I used the unsafe functions instead.[2] - Idris has some nice editor functionality to stub out functions and case splits for you. [1]: Idris2 defaults to "covering", which says case splits have to cover, but relaxes termination checking. A couple of the spots where I put partial in lean could be proven total, but I was not familiar with the theorem proving corner of lean. Idris totality checking is slightly different in that you can't add proofs, but I think you can achieve the same results by adding additional arguments. [2]: Because I didn't know the theorem proving bits, but I intend to go back and try to patch these up as an exercise.