joneugster
commented
6 months ago Thanks for the report. It would be better placed here: https://github.com/Trequetrum/lean4game-logic/issues
Note that the four games are designed by three independent people. I myself, I'm only working on the framework itself (which is what this repo is) and and the game "Robo". Therefore, I don't really have influence on the other games' content.
If you want to see the author's sample solution, it is here: solution level 5/7, and it's quite something to process :)
I got stuck on Level 5 / 7 : Rewriting on the final world (World: Redux: ↔ World Tactics).
Can't think of anything to use "apply" on , and no alternative ideas due to limited tactics. I admit I might be missing something very obvious but it's out of my reach, although I'd still like to check whether it's a problem with the level.
Overall speaking, I feel like the logic game is much less polished than the natural number game and the set theory game (which I both completed). Particularly compared to the set theory game, many similar theorems have inconsistent names (e.g. And.intro vs and_intro).
The instructions also is confusing at times, I don't find the analogies particularly helpful, but I can understand if they're aimed at a less experienced audience, yet the levels themselves seem to assume a familiarity with lambda calculus. I think it'll be much more helpful if the learning curve on lambda notation can be smoothed out.