		Search-engine friendly clone of the ACL2 documentation.

Tokens

Vl-token->string

Get the original text that gave rise to any token, as a string.

Signature
(vl-token->string x) → str
Arguments: x — Guard (vl-token-p x).
Returns: str — Type (stringp str).

Definitions and Theorems

Function: vl-token->string

(defun vl-token->string (x)
  (declare (xargs :guard (vl-token-p x)))
  (let ((__function__ 'vl-token->string))
    (declare (ignorable __function__))
    (vl-echarlist->string (vl-token->etext x))))

Theorem: stringp-of-vl-token->string

(defthm stringp-of-vl-token->string
  (b* ((str (vl-token->string x)))
    (stringp str))
  :rule-classes :type-prescription)