		Search-engine friendly clone of the ACL2 documentation.

Inject-warnings

Vl-warning->loc

Return the location of a warning, if it obeys the location convention.

Signature
(vl-warning->loc x) → loc?
Arguments: x — Guard (vl-warning-p x).
Returns: loc? — Type (iff (vl-location-p loc?) loc?).

Definitions and Theorems

Function: vl-warning->loc

(defun vl-warning->loc (x)
  (declare (xargs :guard (vl-warning-p x)))
  (let ((__function__ 'vl-warning->loc))
    (declare (ignorable __function__))
    (b* ((args (vl-warning->args x)))
      (and (consp args)
           (vl-location-p (car args))
           (car args)))))

Theorem: return-type-of-vl-warning->loc

(defthm return-type-of-vl-warning->loc
  (b* ((loc? (vl-warning->loc x)))
    (iff (vl-location-p loc?) loc?))
  :rule-classes :rewrite)

Theorem: vl-warning->loc-of-vl-warning-fix-x

(defthm vl-warning->loc-of-vl-warning-fix-x
  (equal (vl-warning->loc (vl-warning-fix x))
         (vl-warning->loc x)))

Theorem: vl-warning->loc-vl-warning-equiv-congruence-on-x

(defthm vl-warning->loc-vl-warning-equiv-congruence-on-x
  (implies (vl-warning-equiv x x-equiv)
           (equal (vl-warning->loc x)
                  (vl-warning->loc x-equiv)))
  :rule-classes :congruence)