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

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

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

Closed Laurens-Klijn closed 3 months ago

Laurens-Klijn commented 4 months ago

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

joneugster commented 3 months ago

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?

Laurens-Klijn commented 3 months ago

It works now