Hacker News Reader

I learned coq as a teenager because the name was funny and one defined everything in terms of the `succ` function.

Never underestimate our motivation.

Continuing to do things only because they’re funny as an adult is one of life’s little treats!

Unfortunately, they changed the name to Rocq.

...as long as they also changed the defining function to `hard`, we're still good.