(vl-property-binaryop->string x) → ans
Function:
(defun vl-property-binaryop->string (x) (declare (xargs :guard (vl-property-binaryop-p x))) (let ((__function__ 'vl-property-binaryop->string)) (declare (ignorable __function__)) (case (vl-property-binaryop-fix x) (:vl-prop-and "and") (:vl-prop-intersect "intersect") (:vl-prop-or "or") (:vl-prop-within "within") (:vl-prop-iff "iff") (:vl-prop-until "until") (:vl-prop-suntil "s_until") (:vl-prop-untilwith "until_with") (:vl-prop-suntilwith "s_until_with") (:vl-prop-word-implies "implies") (:vl-prop-thin-implies "|->") (:vl-prop-fat-implies "|=>") (:vl-prop-thin-follows "#-#") (:vl-prop-fat-follows "#=#") (otherwise (progn$ (impossible) "")))))
Theorem:
(defthm stringp-of-vl-property-binaryop->string (b* ((ans (vl-property-binaryop->string x))) (stringp ans)) :rule-classes :type-prescription)
Theorem:
(defthm vl-property-binaryop->string-of-vl-property-binaryop-fix-x (equal (vl-property-binaryop->string (vl-property-binaryop-fix x)) (vl-property-binaryop->string x)))
Theorem:
(defthm vl-property-binaryop->string-vl-property-binaryop-equiv-congruence-on-x (implies (vl-property-binaryop-equiv x x-equiv) (equal (vl-property-binaryop->string x) (vl-property-binaryop->string x-equiv))) :rule-classes :congruence)