Ruleset Triggers #
Triggers are still not enough yet. We introduce one more layer on top, which we call RTrigger for Ruleset Trigger.
It makes sense that, when we want to chase a set of rules, we only consider triggers that feature rules that indeed occur in the rule set.
We capture this simply in a subtype.
@[reducible, inline]
abbrev
RTrigger
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
(obs : LaxObsolescenceCondition sig)
(rs : RuleSet sig)
:
Type (max 0 (max u_3 u_2) u_1)
An RTrigger for a RuleSet $R$ is a Trigger with a rule in $R$.
Instances For
@[reducible, inline]
abbrev
RTrigger.equiv
{sig : Signature}
[DecidableEq sig.P]
[DecidableEq sig.C]
[DecidableEq sig.V]
{obs : LaxObsolescenceCondition sig}
{rs : RuleSet sig}
(trg1 trg2 : RTrigger obs rs)
:
Two RTriggers are equivalent if the underlying PreTriggers are.