What is the real difference between rocq vs lean? Alternatively, what is your motivation to do this in lean as compared to playing around with the rocq one if it exists?
I recently completed the natural number lean game and found it pretty fun, and would like to learn more about the differences between the two. Thanks!
I don’t know about their motivation, but I would say mine is that Lean is a real programming language. Coq is not really meant for “prosaic” programming, more’s the pity.
Lean is also a lot faster.