Victory condition achieved when writing non sensical tactics

[astrale-sharp]

typing rw [mul_succ ()] where mul_succ could be any other valid condition prompts the level to tell you that you won.

Having a blast with this game btw, thanks

[TentativeConvert]

I cannot reproduce this. Which level were you on, and which sequence of tactics did you enter?

[astrale-sharp]

one of many examples : Note that the next button is gray and so you cannot proceed even though you have a winning screen

[joneugster]

I would guess this happens if the game mode is set to "relaxed" and the Lean server actually inserts a sorry instead of throwing an error. Which it does here and there, mainly to make editing Lean files in VSCode nicer.

[kbuzzard]

I am seeing students doing stuff like rw [succ_add_eq_one] (a mis-spelling of succ_eq_add_one) and the game basically freezing -- the goal is repeated and there's no box to type in anything else and there's no error. This is leading to a frustrating user experience :-/

[TentativeConvert]

This appears to be a variant of https://github.com/leanprover-community/lean4game/issues/400 and should be closed here in favour of that issue.