		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-filename-to-string-literal

Signature
(vl-filename-to-string-literal filename) → string
Arguments: filename — Guard (stringp filename).
Returns: string — Type (stringp string).

Definitions and Theorems

Function: vl-filename-to-string-literal

(defun vl-filename-to-string-literal (filename)
 (declare (xargs :guard (stringp filename)))
 (let ((__function__ 'vl-filename-to-string-literal))
   (declare (ignorable __function__))
   (implode
        (append (vl-maybe-escape-string filename 0 (length filename)
                                        (list #\"))
                (list #\")))))

Theorem: stringp-of-vl-filename-to-string-literal

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