Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
joneugster opened this issue Jun 14, 2024 · 1 comment
Open

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

joneugster opened this issue Jun 14, 2024 · 1 comment
Labels
client Functionality of the client side code enhancement New feature or request priority-low nice to have server Concerning the lean gameserver

Comments

@joneugster
Copy link
Collaborator

joneugster commented Jun 14, 2024

"solution" button that automatically shows the intended next step

@joneugster joneugster added enhancement New feature or request client Functionality of the client side code server Concerning the lean gameserver priority-low nice to have labels Jun 14, 2024
@TentativeConvert
Copy link
Collaborator

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.”)

@TentativeConvert TentativeConvert changed the title "solution" button that automatically shows the intended next step "solution" button/indicator light for next intended next step Jul 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
client Functionality of the client side code enhancement New feature or request priority-low nice to have server Concerning the lean gameserver
Projects
None yet
Development

No branches or pull requests

2 participants