		Search-engine friendly clone of the ACL2 documentation.

Closure

Rulelist-unused-rules

Rule names that are defined in a list of rules but not used anywhere in those rules.

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

It is not uncommon for this set to be non-empty. First, top-level rule names are often not used in other rules. Second, sometimes grammars define certain rules to establish nomenclatures, even if those rules may not be used explicitly in other rules.

Definitions and Theorems

Function: rulelist-unused-rules

(defun rulelist-unused-rules (rules)
  (declare (xargs :guard (rulelistp rules)))
  (difference (rulelist-defined-rules rules)
              (rulelist-called-rules rules)))

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

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