leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
137 stars 25 forks source link

Player proceeds after error #233

Open joneugster opened 1 month ago

joneugster commented 1 month ago

See this discussion: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Natural.20Number.20Game.20question/near/440803763

That is not a state the user should end up with, i.e. make sure a user cannot proceed after an error, also not by toggling editor mode.