search

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
Apache License 2.0
292 stars 73 forks source link

Fix missing word in intro.lean #128

Open vezwork opened 1 year ago

vezwork commented 1 year ago

I have just started playing the the natural number game at https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/.

I was reading the intro and noticed a word missing in the following sentence:

In this game, you get own version of the natural numbers, called mynat, in an interactive theorem prover called Lean.

It seems that there is a missing word before own. Should it be

In this game, you get your own version [..]

?

Thank you for reviewing my proposed fix.