		Search-engine friendly clone of the ACL2 documentation.

Closure

Rulelist-called-rules

Rule names that occur in (the definientia of) a list of rules.

Signature
(rulelist-called-rules rules) → rulenames
Arguments: rules — Guard (rulelistp rules).
Returns: rulenames — Type (rulename-setp rulenames).

Definitions and Theorems

Function: rulelist-called-rules

(defun rulelist-called-rules (rules)
  (declare (xargs :guard (rulelistp rules)))
  (cond ((endp rules) nil)
        (t (union (rule-called-rules (car rules))
                  (rulelist-called-rules (cdr rules))))))

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

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