Remove from a list of rules all the ones that define one of the given rule names.
(remove-rules-that-define rulenames rules) → new-rules
Function:
(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:
(defthm rulelistp-of-remove-rules-that-define (b* ((new-rules (remove-rules-that-define rulenames rules))) (rulelistp new-rules)) :rule-classes :rewrite)