leanprover-community/lean4game

Error message "Cannot read properties of undefined (reading 'steps')" when loading "add_mul" level.

Laurens-Klijn opened this issue · 2 comments

I get the "Cannot read properties of undefined (reading 'steps')" When loading the "add_mul" (world 3, level 8).

I'll assume this is the same bug as #201 with repeat rw [] reaching maximum recursion depth. This should now be fixed live. Could you please test and reopen this issue if it still does not work for you?

It works now