(vl-property-acceptop->string x) → ans
Function:
(defun vl-property-acceptop->string (x) (declare (xargs :guard (vl-property-acceptop-p x))) (let ((__function__ 'vl-property-acceptop->string)) (declare (ignorable __function__)) (case (vl-property-acceptop-fix x) (:vl-prop-accepton "accept_on") (:vl-prop-syncaccepton "sync_accept_on") (:vl-prop-rejecton "reject_on") (:vl-prop-syncrejecton "sync_reject_on") (otherwise (progn$ (impossible) "")))))
Theorem:
(defthm stringp-of-vl-property-acceptop->string (b* ((ans (vl-property-acceptop->string x))) (stringp ans)) :rule-classes :type-prescription)
Theorem:
(defthm vl-property-acceptop->string-of-vl-property-acceptop-fix-x (equal (vl-property-acceptop->string (vl-property-acceptop-fix x)) (vl-property-acceptop->string x)))
Theorem:
(defthm vl-property-acceptop->string-vl-property-acceptop-equiv-congruence-on-x (implies (vl-property-acceptop-equiv x x-equiv) (equal (vl-property-acceptop->string x) (vl-property-acceptop->string x-equiv))) :rule-classes :congruence)