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

Categorize tactics according to applicability #52

Open TentativeConvert opened 1 month ago

TentativeConvert commented 1 month ago

Suggestion by a student: put the tactics in the inventory into different categories/tabs according to whether they

I’m not sure this is thought through, but indeed we have quite a few tactics now. (Also, I’m not sure whether the game engine allows putting tactics in different tabs; if not, this issue should perhaps be move to the lean4game repository.)