		Search-engine friendly clone of the ACL2 documentation.

Removal

Remove-rules-that-define

Remove from a list of rules all the ones that define one of the given rule names.

Signature
(remove-rules-that-define rulenames rules) → new-rules
Arguments: rulenames — Guard (rulename-setp rulenames).; rules — Guard (rulelistp rules).
Returns: new-rules — Type (rulelistp new-rules).

Definitions and Theorems

Function: remove-rules-that-define

(defun remove-rules-that-define (rulenames rules)
 (declare (xargs :guard (and (rulename-setp rulenames)
                             (rulelistp rules))))
 (cond
    ((endp rules) nil)
    (t (if (in (rule->name (car rules)) rulenames)
           (remove-rules-that-define rulenames (cdr rules))
         (cons (rule-fix (car rules))
               (remove-rules-that-define rulenames (cdr rules)))))))

Theorem: rulelistp-of-remove-rules-that-define

(defthm rulelistp-of-remove-rules-that-define
  (b* ((new-rules (remove-rules-that-define rulenames rules)))
    (rulelistp new-rules))
  :rule-classes :rewrite)