		Search-engine friendly clone of the ACL2 documentation.

Lint-warning-suppression

Vl-warning-type-mash

Signature
(vl-warning-type-mash x) → mashed
Arguments: x — Guard (symbolp x).
Returns: mashed — Type (stringp mashed).

Definitions and Theorems

Function: vl-warning-type-mash

(defun vl-warning-type-mash (x)
  (declare (xargs :guard (symbolp x)))
  (let ((__function__ 'vl-warning-type-mash))
    (declare (ignorable __function__))
    (vl-mash-warning-string (symbol-name x))))

Theorem: stringp-of-vl-warning-type-mash

(defthm stringp-of-vl-warning-type-mash
  (b* ((mashed (vl-warning-type-mash x)))
    (stringp mashed))
  :rule-classes :type-prescription)

Theorem: vl-warning-type-mash-of-symbol-fix-x

(defthm vl-warning-type-mash-of-symbol-fix-x
  (equal (vl-warning-type-mash (acl2::symbol-fix x))
         (vl-warning-type-mash x)))

Theorem: vl-warning-type-mash-symbol-equiv-congruence-on-x

(defthm vl-warning-type-mash-symbol-equiv-congruence-on-x
  (implies (acl2::symbol-equiv x x-equiv)
           (equal (vl-warning-type-mash x)
                  (vl-warning-type-mash x-equiv)))
  :rule-classes :congruence)