search

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
https://adam.math.hhu.de
Apache License 2.0
16 stars 9 forks source link

Robotswana 2, 3: lemmas appear in inventory before the level is completed #34

Closed TentativeConvert closed 3 months ago

TentativeConvert commented 3 months ago

Levels 2 and 3 of Robotswana ask the user to prove certain statements, but the proof simultaneously appears in the inventory. It should only appear once the level is completed.