Yeah it doesn't always work out. To get an extremely homogeneous deck you really need DNA (make a copy if first hand is high card) with Blueprint(s).

Sometimes I like to try ending up with a tiny deck of all the same card. Often I'll speculatively go for King/Queen for the most powerful jokers, though that does make facing The Plant a bit risky. Especially with higher stakes and antes in endless mode there's a fair amount of luck

The LaTeX this exports uses tikz-cd, but it is certainly much easier to use than writing it by hand.

Since it was only triangles for part 1, I did possibly the most inefficient solution of going out three nodes from each key and checking when the start/end was the same, then a bunch of sorting and erasing duplicates.

(Going to leave part 2 for when I finish my port of the pathfinding crate)

I am so glad Drexel decided to keep around free SEPTA for (some) PhD students so I don't have to think about this lol

Eh, I see what you mean, but I think part 1 was meant as a hint of how you could get the correct time programmatically even if you didn't print anything out. I think checking for some measure of density is pretty intuitive.

It seems relatively common in Lean too. People just usually put it above the definition so I didn't realize it worked for any expression

Putting an `open` inside a definition is interesting. It makes sense but I'd never seen it.

Funnily enough, some people seem to really dislike the days with a visual component. After searching manually for a bit, I made a guess that we wanted the frame with the most dense lines and that worked.

Here is my beautiful unicode Christmas tree. (Hopefully the image blurs, they really should add a spoiler tag)

Oh lol, that makes more sense. Posting a link a day for AoC certainly skews the results...

I'm convinced it also includes the text of usernames when you reply, because mine ("chenson") appeared in my cloud lol

One thing I miss is defining a notation at the same time as a typeclass. You sometimes end up with typeclasses whose sole purpose is a one-off notation, which arguably isn't great.

But in general, I love Lean's system of syntax/elaboration. It just feels "right" to me, if a bit arcane at times.

One thing that eluded me was proving termination for the mutually recursive memoized function. Past that, I think you could maybe write a metaprogram to generate these from regular recursive functions, but that's a bit past my ability level.

Out of curiosity I went and checked my wabbit repo, 17 clones there. About half in the code for environments, half in the LLVM, and two in the parser for peeking.

So would Lean's namespaces fall under this, where for instance you can write either `List.map xs` or `xs.map`?

I tend to like it in pipes, especially since they also open namespaces, e.g. `|>.map`. Insensitivity to argument order is nice too.