		Search-engine friendly clone of the ACL2 documentation.

Lint-warning-suppression

Vl-lint-ignore-att-p

Recognize strings that start with lint-ignore or lint_ignore, case insensitive

Signature
(vl-lint-ignore-att-p x) → *
Arguments: x — Guard (stringp x).

Definitions and Theorems

Function: vl-lint-ignore-att-p

(defun vl-lint-ignore-att-p (x)
  (declare (xargs :guard (stringp x)))
  (let ((__function__ 'vl-lint-ignore-att-p))
    (declare (ignorable __function__))
    (b* ((x (string-fix x))
         (x (str::strsubst "-" "_" x)))
      (str::istrprefixp "lint_ignore" x))))

Theorem: vl-lint-ignore-att-p-of-str-fix-x

(defthm vl-lint-ignore-att-p-of-str-fix-x
  (equal (vl-lint-ignore-att-p (str-fix x))
         (vl-lint-ignore-att-p x)))

Theorem: vl-lint-ignore-att-p-streqv-congruence-on-x

(defthm vl-lint-ignore-att-p-streqv-congruence-on-x
  (implies (streqv x x-equiv)
           (equal (vl-lint-ignore-att-p x)
                  (vl-lint-ignore-att-p x-equiv)))
  :rule-classes :congruence)