		Search-engine friendly clone of the ACL2 documentation.

Rule-called-rules

Rule names that occur in (the definiens of) a rule.

Function: rule-called-rules

(defun rule-called-rules (rule)
  (declare (xargs :guard (rulep rule)))
  (alternation-called-rules (rule->definiens rule)))

Theorem: rulename-setp-of-rule-called-rules

(defthm rulename-setp-of-rule-called-rules
  (b* ((rulenames (rule-called-rules rule)))
    (rulename-setp rulenames))
  :rule-classes :rewrite)