Bram-Hub
[ENHANCEMENT] Restrict Rules within Puzzles
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.
Additional Context
No response
