You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Describe the current behavior of what you're trying to improve. If your enhancement request related to a problem, please also describe the problem.
When learning proofs for the first time, only the most basic rules are allowed, like ^ Introduction and ~ Elimination. It would be cool if some puzzles restricted the use of higher-level rules to more closely follow this teaching structure.
It's also nice in cases where a rule doesn't work properly, to prevent students from losing credit for using a broken rule that should work.
Describe the improvement you'd like
Add a tag within a given puzzle file that restricts certain rules. The tag could include the full name of the rule, or just the ID (i.e, NURI-BASC-0001). This should be backward compatible; an older version of LEGUP will simply ignore the additional XML node.
Describe alternatives you've considered
It would be cool if a user could build a specialized rule, similar to how Fitch has lemmas. I have no idea how that would be implemented, though.
Activity