		Search-engine friendly clone of the ACL2 documentation.

Lint-warning-suppression

Vl-lint-attname-says-ignore

Signature
(vl-lint-attname-says-ignore attname mashed-warning-type) → ignorep
Arguments: attname — Guard (stringp attname).; mashed-warning-type — Guard (stringp mashed-warning-type).
Returns: ignorep — Type (booleanp ignorep).

Definitions and Theorems

Function: vl-lint-attname-says-ignore

(defun vl-lint-attname-says-ignore (attname mashed-warning-type)
  (declare (xargs :guard (and (stringp attname)
                              (stringp mashed-warning-type))))
  (let ((__function__ 'vl-lint-attname-says-ignore))
    (declare (ignorable __function__))
    (b* (((unless (vl-lint-ignore-att-p attname))
          nil)
         (mashed-att (vl-lint-ignore-att-mash attname))
         ((when (equal mashed-att "")) t))
      (str::istrprefixp mashed-att mashed-warning-type))))

Theorem: booleanp-of-vl-lint-attname-says-ignore

(defthm booleanp-of-vl-lint-attname-says-ignore
  (b*
   ((ignorep
         (vl-lint-attname-says-ignore attname mashed-warning-type)))
   (booleanp ignorep))
  :rule-classes :type-prescription)