		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-string-expr->value

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

Definitions and Theorems

Function: vl-string-expr->value

(defun vl-string-expr->value (x)
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-string-expr->value))
    (declare (ignorable __function__))
    (vl-expr-case x
                  :vl-literal (vl-value-case x.val
                                             :vl-string x.val.value
                                             :otherwise nil)
                  :otherwise nil)))

Theorem: maybe-stringp-of-vl-string-expr->value

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

Theorem: vl-string-expr->value-of-vl-expr-fix-x

(defthm vl-string-expr->value-of-vl-expr-fix-x
  (equal (vl-string-expr->value (vl-expr-fix x))
         (vl-string-expr->value x)))

Theorem: vl-string-expr->value-vl-expr-equiv-congruence-on-x

(defthm vl-string-expr->value-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-string-expr->value x)
                  (vl-string-expr->value x-equiv)))
  :rule-classes :congruence)