[jjmarr]

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.

[knotimpressed]

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

[jjmarr]

Unfortunately, they changed the name to Rocq.

[kleiba]

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