Function:
(defun vl-filename-to-suppress-p-aux (filename suppress-filename) (declare (xargs :guard (and (stringp filename) (stringp suppress-filename)))) (let ((__function__ 'vl-filename-to-suppress-p-aux)) (declare (ignorable __function__)) (b* ((filename (string-fix filename)) (suppress-filename (string-fix suppress-filename)) ((when (str::strprefixp "/" suppress-filename)) (equal filename suppress-filename))) (str::strsuffixp suppress-filename filename))))
Theorem:
(defthm booleanp-of-vl-filename-to-suppress-p-aux (b* ((suppress-p (vl-filename-to-suppress-p-aux filename suppress-filename))) (booleanp suppress-p)) :rule-classes :type-prescription)
Theorem:
(defthm vl-filename-to-suppress-p-aux-of-str-fix-filename (equal (vl-filename-to-suppress-p-aux (str-fix filename) suppress-filename) (vl-filename-to-suppress-p-aux filename suppress-filename)))
Theorem:
(defthm vl-filename-to-suppress-p-aux-streqv-congruence-on-filename (implies (streqv filename filename-equiv) (equal (vl-filename-to-suppress-p-aux filename suppress-filename) (vl-filename-to-suppress-p-aux filename-equiv suppress-filename))) :rule-classes :congruence)
Theorem:
(defthm vl-filename-to-suppress-p-aux-of-str-fix-suppress-filename (equal (vl-filename-to-suppress-p-aux filename (str-fix suppress-filename)) (vl-filename-to-suppress-p-aux filename suppress-filename)))
Theorem:
(defthm vl-filename-to-suppress-p-aux-streqv-congruence-on-suppress-filename (implies (streqv suppress-filename suppress-filename-equiv) (equal (vl-filename-to-suppress-p-aux filename suppress-filename) (vl-filename-to-suppress-p-aux filename suppress-filename-equiv))) :rule-classes :congruence)