		Search-engine friendly clone of the ACL2 documentation.

Vl-location

Vl-location->filename

Get the filename from a vl-location.

Signature
(vl-location->filename x) → filename
Arguments: x — Guard (vl-location-p x).
Returns: filename — Type (stringp filename).

Definitions and Theorems

Function: vl-location->filename$inline

(defun vl-location->filename$inline (x)
  (declare (xargs :guard (vl-location-p x)))
  (let ((__function__ 'vl-location->filename))
    (declare (ignorable __function__))
    (cddr (vl-location-fix x))))

Theorem: stringp-of-vl-location->filename

(defthm stringp-of-vl-location->filename
  (b* ((filename (vl-location->filename$inline x)))
    (stringp filename))
  :rule-classes :type-prescription)

Theorem: vl-location->filename-of-vl-location

(defthm vl-location->filename-of-vl-location
  (equal (vl-location->filename (vl-location filename line col))
         (str-fix filename)))