search

leanprover-community / lean4game

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

Robo Anonyme Funktionen 1 crash #249

Closed NoLongerBreathedIn closed 4 months ago

NoLongerBreathedIn commented 4 months ago

I tried the following obvious tactics on Anonymous Function level 1:

use λn↦n-1
intro n
simp

and also replacing simp with linarith.

Both of these cause the game to crash with:

Oops!

Sorry, an unexpected error has occurred.

undefined has no properties

The only way to get out of this is to refresh, switch to text-editor mode, and quickly delete the last command.

TentativeConvert commented 4 months ago

Thanks for the report, which confirms https://github.com/hhu-adam/Robo/issues/56#issuecomment-2222191412.

joneugster commented 4 months ago

Should be fixed, see hhu-adam/Robo#56