Menu
▾
▴
#341 Provide a parameterized tactic for Theory rules
In the current setting, there are only two tactics available from the Theory plug-in. They run either all rewrite rules or all inference rules. It would be very friendly to provide a parameterized tactic that would allow to restrict the rules that would be applied automatically.
I have the feeling that we might need some tactic defined by each theory (or even several tactics for each theory). As far as I remember, the parameterized tactic (the Atelier-B PP and ML) have some "static" parameters, e.g., time-out, pre-defined force. It is not the case for the rule-based provers.
Cheers,
Son