20
π¦ - 2023 DAY 9 SOLUTIONS -π¦
(programming.dev)
An unofficial home for the advent of code community on programming.dev!
Advent of Code is an annual Advent calendar of small programming puzzles for a variety of skill sets and skill levels that can be solved in any programming language you like.
Solution Threads
M | T | W | T | F | S | S |
---|---|---|---|---|---|---|
1 | 2 | 3 | ||||
4 | 5 | 6 | 7 | 8 | 9 | 10 |
11 | 12 | 13 | 14 | 15 | 16 | 17 |
18 | 19 | 20 | 21 | 22 | 23 | 24 |
25 |
Icon base by Lorc under CC BY 3.0 with modifications to add a gradient
console.log('Hello World')
[Language: Lean4]
This one was very easy, almost trivial. Lean4 did demand a proof of termination though, and I'm still not very good at writing proofs...
I'm also pretty happy that this time I was able to re-use most of part 1 for part 2, and part 2 being a one-liner therefore.
As always, here is only the file with the actual solution, some helper functions are implemented in different files - check my github for the whole project.
Solution