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