Get the value field from a vl-string.
(vl-string->value x) → value
This is an ordinary field accessor created by defprod.
Function:
(defun vl-string->value$inline (x) (declare (xargs :guard (vl-value-p x))) (declare (xargs :guard (equal (vl-value-kind x) :vl-string))) (let ((__function__ 'vl-string->value)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and (equal (vl-value-kind x) :vl-string) x))) (str-fix (cdr x))) :exec (cdr x))))
Theorem:
(defthm stringp-of-vl-string->value (b* ((value (vl-string->value$inline x))) (stringp value)) :rule-classes :type-prescription)
Theorem:
(defthm vl-string->value$inline-of-vl-value-fix-x (equal (vl-string->value$inline (vl-value-fix x)) (vl-string->value$inline x)))
Theorem:
(defthm vl-string->value$inline-vl-value-equiv-congruence-on-x (implies (vl-value-equiv x x-equiv) (equal (vl-string->value$inline x) (vl-string->value$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-string->value-when-wrong-kind (implies (not (equal (vl-value-kind x) :vl-string)) (equal (vl-string->value x) (str-fix nil))))