Advent of Code in Lean 4 so far:
day 1: how do I do anything in a language with undocumented standard library???
day 2: this could be actually fun?
day 3: already cheating with "partial def"
day 4: already cheating with imperative code
day 1: how do I do anything in a language with undocumented standard library???
day 2: this could be actually fun?
day 3: already cheating with "partial def"
day 4: already cheating with imperative code
Comments
Lean: sorry, it isn't clear to me that this recursive function always terminates, you have to give a proof of termination, otherwise I won't touch this
me: partial def something …
Lean: lol, actually I don't care, have fun, it's your code