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.

Sign up for GitHub

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

Jump to bottom

feat: DefEq in Hint #45

Open
joneugster opened this issue Mar 7, 2023 · 0 comments
Open

feat: DefEq in Hint #45

joneugster opened this issue Mar 7, 2023 · 0 comments
Labels
enhancement New feature or request fixed on dev Will be part of the next update priority-medium should be addressed within the next months server Concerning the lean gameserver

Comments

@joneugster
Copy link
Collaborator

joneugster commented Mar 7, 2023 •
edited
Loading

The current Hint matches expressions exactly, which allows for detailed instructions about unfold or change.
However, it would be handy to have an option Hint (defeq := true) "some text" to relax this, so that a hint is shown even if the goal is only defEq to the Hint's goal.

Also think about defeq in the assumptions. Currently hints might not be shown if the user unfolds a definition more/less than the sample solution did, for example in the level about Function.Bijective.
@joneugster joneugster added the question Further information is requested label Mar 7, 2023
@joneugster joneugster changed the title feat: DefEq in Hints feat: DefEq in Hint Mar 31, 2023
@joneugster joneugster added enhancement New feature or request server Concerning the lean gameserver priority-medium should be addressed within the next months labels Mar 31, 2023
@joneugster joneugster removed the question Further information is requested label Apr 28, 2023
joneugster added a commit that referenced this issue Jun 6, 2024
@joneugster
add defeq-hints #45
a7d746a
joneugster added a commit that referenced this issue Jun 6, 2024
@joneugster
turn defeq-hints on by default #45
71fad56
@joneugster joneugster added the fixed on dev Will be part of the next update label Jun 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request fixed on dev Will be part of the next update priority-medium should be addressed within the next months server Concerning the lean gameserver
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@joneugster