leanprover-community/lean4game

"solution" button/indicator light for next intended next step

joneugster opened this issue · 1 comments

"solution" button that automatically shows the intended next step

Alternative, similar suggestions:

  • Display a full list of all tactics and theorems used in the intended solution(s).
  • Add a green indicator that turns yellow when the current proof state no longer matches any of the intended states.

(One student who played through Robo reported: “At some point, I made a habit of automatically opening every hidden hint that was offered, just to reassure myself I hadn’t gone completely off track. In hindsight, that was a pity, since in many cases I really did not need that hint.”)