(vl-property-unaryop->string x) → ans
Function:
(defun vl-property-unaryop->string (x) (declare (xargs :guard (vl-property-unaryop-p x))) (let ((__function__ 'vl-property-unaryop->string)) (declare (ignorable __function__)) (case (vl-property-unaryop-fix x) (:vl-prop-firstmatch "first_match") (:vl-prop-not "not") (:vl-prop-strong "strong") (:vl-prop-weak "weak") (otherwise (progn$ (impossible) "")))))
Theorem:
(defthm stringp-of-vl-property-unaryop->string (b* ((ans (vl-property-unaryop->string x))) (stringp ans)) :rule-classes :type-prescription)
Theorem:
(defthm vl-property-unaryop->string-of-vl-property-unaryop-fix-x (equal (vl-property-unaryop->string (vl-property-unaryop-fix x)) (vl-property-unaryop->string x)))
Theorem:
(defthm vl-property-unaryop->string-vl-property-unaryop-equiv-congruence-on-x (implies (vl-property-unaryop-equiv x x-equiv) (equal (vl-property-unaryop->string x) (vl-property-unaryop->string x-equiv))) :rule-classes :congruence)