'generalizing' is locked at the level it is being introduced.

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

'generalizing' is locked at the level it is being introduced. #133

Open zadeoglu opened 9 months ago

zadeoglu commented 9 months ago

Attached is a screenshot of the issue I am having. Instructions tell me to use generalize however the system won't let me. This is in level 9 of the Advanced Multiplication World.

P.S: For other users who are having the same problem. This can be circumvented by changing the game rule settings to "relaxed" in the main menu.

In case it is relevant, the browser is firefox running on linux mint 21.3