(vl-filename-to-suppress-p filename suppress-files) → suppress-p
Function:
(defun vl-filename-to-suppress-p (filename suppress-files) (declare (xargs :guard (and (stringp filename) (string-listp suppress-files)))) (let ((__function__ 'vl-filename-to-suppress-p)) (declare (ignorable __function__)) (if (atom suppress-files) nil (or (vl-filename-to-suppress-p-aux filename (car suppress-files)) (vl-filename-to-suppress-p filename (cdr suppress-files))))))
Theorem:
(defthm booleanp-of-vl-filename-to-suppress-p (b* ((suppress-p (vl-filename-to-suppress-p filename suppress-files))) (booleanp suppress-p)) :rule-classes :type-prescription)
Theorem:
(defthm vl-filename-to-suppress-p-of-str-fix-filename (equal (vl-filename-to-suppress-p (str-fix filename) suppress-files) (vl-filename-to-suppress-p filename suppress-files)))
Theorem:
(defthm vl-filename-to-suppress-p-streqv-congruence-on-filename (implies (streqv filename filename-equiv) (equal (vl-filename-to-suppress-p filename suppress-files) (vl-filename-to-suppress-p filename-equiv suppress-files))) :rule-classes :congruence)
Theorem:
(defthm vl-filename-to-suppress-p-of-string-list-fix-suppress-files (equal (vl-filename-to-suppress-p filename (string-list-fix suppress-files)) (vl-filename-to-suppress-p filename suppress-files)))
Theorem:
(defthm vl-filename-to-suppress-p-string-list-equiv-congruence-on-suppress-files (implies (str::string-list-equiv suppress-files suppress-files-equiv) (equal (vl-filename-to-suppress-p filename suppress-files) (vl-filename-to-suppress-p filename suppress-files-equiv))) :rule-classes :congruence)