		Search-engine friendly clone of the ACL2 documentation.

Vl-warninglist

Vl-warnings-to-string

Pretty-print a vl-warninglist into a string.

Signature
(vl-warnings-to-string warnings) → str
Arguments: warnings — Guard (vl-warninglist-p warnings).
Returns: str — Type (stringp str).

See vl-print-warnings-with-header and with-local-ps.

Definitions and Theorems

Function: vl-warnings-to-string

(defun vl-warnings-to-string (warnings)
  (declare (xargs :guard (vl-warninglist-p warnings)))
  (let ((__function__ 'vl-warnings-to-string))
    (declare (ignorable __function__))
    (with-local-ps (vl-print-warnings-with-header warnings))))

Theorem: stringp-of-vl-warnings-to-string

(defthm stringp-of-vl-warnings-to-string
  (b* ((str (vl-warnings-to-string warnings)))
    (stringp str))
  :rule-classes :type-prescription)

Theorem: vl-warnings-to-string-of-vl-warninglist-fix-warnings

(defthm vl-warnings-to-string-of-vl-warninglist-fix-warnings
  (equal (vl-warnings-to-string (vl-warninglist-fix warnings))
         (vl-warnings-to-string warnings)))

Theorem: vl-warnings-to-string-vl-warninglist-equiv-congruence-on-warnings

(defthm
  vl-warnings-to-string-vl-warninglist-equiv-congruence-on-warnings
  (implies (vl-warninglist-equiv warnings warnings-equiv)
           (equal (vl-warnings-to-string warnings)
                  (vl-warnings-to-string warnings-equiv)))
  :rule-classes :congruence)